Struct Term

Source

pub struct Term { /* private fields */ }

Expand description

A term in first-order logic.

Terms represent objects in the domain of discourse. A term can be:

A constant: socrates
A variable: x
A function application: add(x, y)

§Examples

use vampire_prover::{Function, Term};

// Create a constant
let zero = Function::constant("0");

// Create a variable
let x = Term::new_var(0);

// Create a function application
let succ = Function::new("succ", 1);
let one = succ.with(zero);

Implementations§

Source §

impl Term

Source

pub fn new_function(func: Function, args: &[Term]) -> Self

Creates a term by applying a function to arguments.

This is typically called via Function::with rather than directly.

§Panics

Panics if the number of arguments does not match the function’s arity.

§Examples

use vampire_prover::{Function, Term};

let add = Function::new("add", 2);
let x = Term::new_var(0);
let y = Term::new_var(1);

let sum = Term::new_function(add, &[x, y]);

Source

pub fn new_var(idx: u32) -> Self

Creates a variable with the given index.

Variables are typically used within quantified formulas. The index should be unique within a formula. For automatic variable management, consider using the forall and exists helper functions instead.

§Arguments

idx - The unique index for this variable

§Examples

use vampire_prover::Term;

let x = Term::new_var(0);
let y = Term::new_var(1);

Source

pub fn free_var() -> (Self, u32)

Creates a fresh variable with an automatically assigned index.

Returns both the variable term and its index. This is primarily used internally by the forall and exists functions.

§Examples

use vampire_prover::Term;

let (x, idx) = Term::free_var();
assert_eq!(idx, 0);

let (y, idx2) = Term::free_var();
assert_eq!(idx2, 1);

Source

pub fn eq(&self, rhs: Term) -> Formula

Creates an equality formula between this term and another.

§Arguments

rhs - The right-hand side of the equality

§Examples

use vampire_prover::{Function, forall};

let succ = Function::new("succ", 1);
let zero = Function::constant("0");

// ∀x. succ(x) = succ(x)
let reflexive = forall(|x| {
    let sx = succ.with(x);
    sx.eq(sx)
});

Examples found in repository ?

examples/name_reuse.rs (line 21)

3fn main() {
4    let x1 = Function::new("x", 0);
5    let x2 = Function::new("x", 0);
6
7    dbg!(x1, x2);
8    dbg!(x1 == x2);
9
10    let y1 = Function::new("y", 0);
11    let y2 = Function::new("y", 1);
12
13    dbg!(y1, y2);
14
15    let z1 = Function::new("z", 0);
16    let z2 = Predicate::new("z", 0);
17
18    dbg!(z1, z2);
19
20    let solution = Problem::new(Options::new())
21        .with_axiom(y1.with(&[]).eq(y2.with(&[y1.with(&[])])))
22        .solve();
23
24    dbg!(solution);
25}

More examples

Hide additional examples

examples/bench_index2.rs (line 123)

113fn run_proof(i: usize) -> ProofRes {
114    // Prove that every subgroup of index 2 is normal.
115    let mult = Function::new(&format!("mult{i}"), 2);
116    let inv = Function::new(&format!("inv{i}"), 1);
117    let one = Function::constant(&format!("1{i}"));
118
119    // Helper to make multiplication more readable
120    let mul = |x: Term, y: Term| -> Term { mult.with(&[x, y]) };
121
122    // Group Axiom 1: Right identity - ∀x. x * 1 = x
123    let right_identity = forall(|x| mul(x, one).eq(x));
124
125    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
126    let right_inverse = forall(|x| {
127        let inv_x = inv.with(&[x]);
128        mul(x, inv_x).eq(one)
129    });
130
131    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
132    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));
133
134    // Describe the subgroup
135    let h = Predicate::new("h", 1);
136
137    // Any subgroup contains the identity
138    let h_ident = h.with(&[one]);
139
140    // And is closed under multiplication
141    let h_mul_closed =
142        forall(|x| forall(|y| (h.with(&[x]) & h.with(&[y])) >> h.with(&[mul(x, y)])));
143
144    // And is closed under inverse
145    let h_inv_closed = forall(|x| h.with(&[x]) >> h.with(&[inv.with(&[x])]));
146
147    // H specifically is of order 2
148    let h_index_2 = exists(|x| {
149        // an element not in H
150        let not_in_h = !h.with(&[x]);
151        // but everything is in H or x H
152        let class = forall(|y| h.with(&[y]) | h.with(&[mul(inv.with(&[x]), y)]));
153
154        not_in_h & class
155    });
156
157    // Conjecture: H is normal
158    let h_normal = forall(|x| {
159        let h_x = h.with(&[x]);
160        let conj_x = forall(|y| {
161            let y_inv = inv.with(&[y]);
162            h.with(&[mul(mul(y, x), y_inv)])
163        });
164        h_x.iff(conj_x)
165    });
166
167    Problem::new(Options::new())
168        .with_axiom(right_identity)
169        .with_axiom(right_inverse)
170        .with_axiom(associativity)
171        .with_axiom(h_ident)
172        .with_axiom(h_mul_closed)
173        .with_axiom(h_inv_closed)
174        .with_axiom(h_index_2)
175        .conjecture(h_normal)
176        .solve()
177}