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 to_string(&self) -> String

Converts this term to a string representation.

§Panics

Panics if the underlying C API fails (which should never happen in normal use).

§Examples

use vampire_prover::Function;

let x = Function::constant("x");
println!("{}", x.to_string()); // Prints the vampire string representation

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/group.rs (line 19)

3fn main() {
4    // Prove that the identity element works on the left using group axioms
5    // In group theory, if we define a group with:
6    //   - Right identity: x * 1 = x
7    //   - Right inverse: x * inv(x) = 1
8    //   - Associativity: (x * y) * z = x * (y * z)
9    // Then we can prove the left identity: 1 * x = x
10
11    let mult = Function::new("mult", 2);
12    let inv = Function::new("inv", 1);
13    let one = Function::constant("1");
14
15    // Helper to make multiplication more readable
16    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };
17
18    // Axiom 1: Right identity - ∀x. x * 1 = x
19    let right_identity = forall(|x| mul(x, one).eq(x));
20
21    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
22    let right_inverse = forall(|x| {
23        let inv_x = inv.with(x);
24        mul(x, inv_x).eq(one)
25    });
26
27    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
28    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));
29
30    // Conjecture: Left identity - ∀x. 1 * x = x
31    let left_identity = forall(|x| mul(one, x).eq(x));
32
33    let (solution, proof) = Problem::new(Options::new())
34        .with_axiom(right_identity)
35        .with_axiom(right_inverse)
36        .with_axiom(associativity)
37        .conjecture(left_identity)
38        .solve_and_prove();
39
40    if let Some(proof) = proof {
41        println!("{}", proof);
42    }
43
44    assert_eq!(solution, ProofRes::Proved);
45}

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}

examples/group2.rs (line 13)

3fn main() {
4    // Prove that every subgroup of index 2 is normal.
5    let mult = Function::new("mult", 2);
6    let inv = Function::new("inv", 1);
7    let one = Function::constant("1");
8
9    // Helper to make multiplication more readable
10    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };
11
12    // Group Axiom 1: Right identity - ∀x. x * 1 = x
13    let right_identity = forall(|x| mul(x, one).eq(x));
14
15    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
16    let right_inverse = forall(|x| {
17        let inv_x = inv.with(x);
18        mul(x, inv_x).eq(one)
19    });
20
21    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
22    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));
23
24    // Describe the subgroup
25    let h = Predicate::new("h", 1);
26
27    // Any subgroup contains the identity
28    let h_ident = h.with(one);
29
30    // And is closed under multiplication
31    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));
32
33    // And is closed under inverse
34    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));
35
36    // H specifically is of order 2
37    let h_index_2 = exists(|x| {
38        // an element not in H
39        let not_in_h = !h.with(x);
40        // but everything is in H or x H
41        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));
42
43        not_in_h & class
44    });
45
46    // Conjecture: H is normal
47    let h_normal = forall(|x| {
48        let h_x = h.with(x);
49        let conj_x = forall(|y| {
50            let y_inv = inv.with(y);
51            h.with(mul(mul(y, x), y_inv))
52        });
53        h_x.iff(conj_x)
54    });
55
56    let (solution, proof) = Problem::new(Options::new())
57        .with_axiom(right_identity)
58        .with_axiom(right_inverse)
59        .with_axiom(associativity)
60        .with_axiom(h_ident)
61        .with_axiom(h_mul_closed)
62        .with_axiom(h_inv_closed)
63        .with_axiom(h_index_2)
64        .conjecture(h_normal)
65        .solve_and_prove();
66
67    if let Some(proof) = proof {
68        println!("{}", proof);
69    }
70
71    assert_eq!(solution, ProofRes::Proved);
72}