Struct Problem 

pub struct Problem { /* private fields */ }

A theorem proving problem consisting of axioms and an optional conjecture.

A Problem is constructed by adding axioms (assumed to be true) and optionally a conjecture (the statement to be proved). The problem is then solved by calling Problem::solve, which invokes the Vampire theorem prover.

Examples

Basic Usage

use vampire_prover::{Function, Predicate, Problem, ProofRes, Options, forall};

let mortal = Predicate::new("mortal", 1);
let human = Predicate::new("human", 1);
let socrates = Function::constant("socrates");

let result = Problem::new(Options::new())
    .with_axiom(human.with(socrates))
    .with_axiom(forall(|x| human.with(x) >> mortal.with(x)))
    .conjecture(mortal.with(socrates))
    .solve();

assert_eq!(result, ProofRes::Proved);

Without Conjecture

You can also create problems without a conjecture to check satisfiability:

use vampire_prover::{Function, Predicate, Problem, Options};

let p = Predicate::new("P", 1);
let x = Function::constant("x");

let result = Problem::new(Options::new())
    .with_axiom(p.with(x))
    .with_axiom(!p.with(x))  // Contradiction
    .solve();

// This should be unsatisfiable

Implementations

impl Problem

pub fn new(options: Options) -> Self

Creates a new empty problem with the given options.

Arguments

• options - Configuration options for the prover

Examples

use vampire_prover::{Problem, Options};
use std::time::Duration;

// Default options
let problem = Problem::new(Options::new());

Examples found in repository

examples/name_reuse.rs (line 20)

fn main() {
    let x1 = Function::new("x", 0);
    let x2 = Function::new("x", 0);

    dbg!(x1, x2);
    dbg!(x1 == x2);

    let y1 = Function::new("y", 0);
    let y2 = Function::new("y", 1);

    dbg!(y1, y2);

    let z1 = Function::new("z", 0);
    let z2 = Predicate::new("z", 0);

    dbg!(z1, z2);

    let solution = Problem::new(Options::new())
        .with_axiom(y1.with(&[]).eq(y2.with(&[y1.with(&[])])))
        .solve();

    dbg!(solution);
}

examples/group.rs (line 33)

fn main() {
    // Prove that the identity element works on the left using group axioms
    // In group theory, if we define a group with:
    //   - Right identity: x * 1 = x
    //   - Right inverse: x * inv(x) = 1
    //   - Associativity: (x * y) * z = x * (y * z)
    // Then we can prove the left identity: 1 * x = x

    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Conjecture: Left identity - ∀x. 1 * x = x
    let left_identity = forall(|x| mul(one, x).eq(x));

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .conjecture(left_identity)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

examples/bench_index2.rs (line 167)

fn run_proof(i: usize) -> ProofRes {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new(&format!("mult{i}"), 2);
    let inv = Function::new(&format!("inv{i}"), 1);
    let one = Function::constant(&format!("1{i}"));

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with(&[x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(&[x]);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(&[one]);

    // And is closed under multiplication
    let h_mul_closed =
        forall(|x| forall(|y| (h.with(&[x]) & h.with(&[y])) >> h.with(&[mul(x, y)])));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(&[x]) >> h.with(&[inv.with(&[x])]));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(&[x]);
        // but everything is in H or x H
        let class = forall(|y| h.with(&[y]) | h.with(&[mul(inv.with(&[x]), y)]));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(&[x]);
        let conj_x = forall(|y| {
            let y_inv = inv.with(&[y]);
            h.with(&[mul(mul(y, x), y_inv)])
        });
        h_x.iff(conj_x)
    });

    Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve()
}

examples/group2.rs (line 56)

fn main() {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(one);

    // And is closed under multiplication
    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(x);
        // but everything is in H or x H
        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(x);
        let conj_x = forall(|y| {
            let y_inv = inv.with(y);
            h.with(mul(mul(y, x), y_inv))
        });
        h_x.iff(conj_x)
    });

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

pub fn with_axiom(&mut self, f: Formula) -> &mut Self

Adds an axiom to the problem.

Axioms are formulas assumed to be true. The prover will use these axioms to attempt to prove the conjecture (if one is provided).

This method consumes self and returns a new Problem, allowing for method chaining.

Arguments

• f - The axiom formula to add

Examples

use vampire_prover::{Function, Predicate, Problem, Options, forall};

let p = Predicate::new("P", 1);
let q = Predicate::new("Q", 1);

let problem = Problem::new(Options::new())
    .with_axiom(forall(|x| p.with(x)))
    .with_axiom(forall(|x| p.with(x) >> q.with(x)));

Examples found in repository

examples/name_reuse.rs (line 21)

fn main() {
    let x1 = Function::new("x", 0);
    let x2 = Function::new("x", 0);

    dbg!(x1, x2);
    dbg!(x1 == x2);

    let y1 = Function::new("y", 0);
    let y2 = Function::new("y", 1);

    dbg!(y1, y2);

    let z1 = Function::new("z", 0);
    let z2 = Predicate::new("z", 0);

    dbg!(z1, z2);

    let solution = Problem::new(Options::new())
        .with_axiom(y1.with(&[]).eq(y2.with(&[y1.with(&[])])))
        .solve();

    dbg!(solution);
}

examples/group.rs (line 34)

fn main() {
    // Prove that the identity element works on the left using group axioms
    // In group theory, if we define a group with:
    //   - Right identity: x * 1 = x
    //   - Right inverse: x * inv(x) = 1
    //   - Associativity: (x * y) * z = x * (y * z)
    // Then we can prove the left identity: 1 * x = x

    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Conjecture: Left identity - ∀x. 1 * x = x
    let left_identity = forall(|x| mul(one, x).eq(x));

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .conjecture(left_identity)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

examples/bench_index2.rs (line 168)

fn run_proof(i: usize) -> ProofRes {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new(&format!("mult{i}"), 2);
    let inv = Function::new(&format!("inv{i}"), 1);
    let one = Function::constant(&format!("1{i}"));

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with(&[x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(&[x]);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(&[one]);

    // And is closed under multiplication
    let h_mul_closed =
        forall(|x| forall(|y| (h.with(&[x]) & h.with(&[y])) >> h.with(&[mul(x, y)])));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(&[x]) >> h.with(&[inv.with(&[x])]));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(&[x]);
        // but everything is in H or x H
        let class = forall(|y| h.with(&[y]) | h.with(&[mul(inv.with(&[x]), y)]));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(&[x]);
        let conj_x = forall(|y| {
            let y_inv = inv.with(&[y]);
            h.with(&[mul(mul(y, x), y_inv)])
        });
        h_x.iff(conj_x)
    });

    Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve()
}

examples/group2.rs (line 57)

fn main() {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(one);

    // And is closed under multiplication
    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(x);
        // but everything is in H or x H
        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(x);
        let conj_x = forall(|y| {
            let y_inv = inv.with(y);
            h.with(mul(mul(y, x), y_inv))
        });
        h_x.iff(conj_x)
    });

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

pub fn conjecture(&mut self, f: Formula) -> &mut Self

Sets the conjecture for the problem.

The conjecture is the statement that the prover will attempt to prove from the axioms. A problem can have at most one conjecture.

This method consumes self and returns a new Problem, allowing for method chaining.

Arguments

• f - The conjecture formula

Examples

use vampire_prover::{Function, Predicate, Problem, Options, forall};

let p = Predicate::new("P", 1);
let q = Predicate::new("Q", 1);

let problem = Problem::new(Options::new())
    .with_axiom(forall(|x| p.with(x) >> q.with(x)))
    .conjecture(forall(|x| q.with(x)));  // Try to prove this

Examples found in repository

examples/group.rs (line 37)

fn main() {
    // Prove that the identity element works on the left using group axioms
    // In group theory, if we define a group with:
    //   - Right identity: x * 1 = x
    //   - Right inverse: x * inv(x) = 1
    //   - Associativity: (x * y) * z = x * (y * z)
    // Then we can prove the left identity: 1 * x = x

    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Conjecture: Left identity - ∀x. 1 * x = x
    let left_identity = forall(|x| mul(one, x).eq(x));

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .conjecture(left_identity)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

examples/bench_index2.rs (line 175)

fn run_proof(i: usize) -> ProofRes {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new(&format!("mult{i}"), 2);
    let inv = Function::new(&format!("inv{i}"), 1);
    let one = Function::constant(&format!("1{i}"));

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with(&[x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(&[x]);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(&[one]);

    // And is closed under multiplication
    let h_mul_closed =
        forall(|x| forall(|y| (h.with(&[x]) & h.with(&[y])) >> h.with(&[mul(x, y)])));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(&[x]) >> h.with(&[inv.with(&[x])]));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(&[x]);
        // but everything is in H or x H
        let class = forall(|y| h.with(&[y]) | h.with(&[mul(inv.with(&[x]), y)]));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(&[x]);
        let conj_x = forall(|y| {
            let y_inv = inv.with(&[y]);
            h.with(&[mul(mul(y, x), y_inv)])
        });
        h_x.iff(conj_x)
    });

    Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve()
}

examples/group2.rs (line 64)

fn main() {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(one);

    // And is closed under multiplication
    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(x);
        // but everything is in H or x H
        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(x);
        let conj_x = forall(|y| {
            let y_inv = inv.with(y);
            h.with(mul(mul(y, x), y_inv))
        });
        h_x.iff(conj_x)
    });

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

pub fn solve(&mut self) -> ProofRes

Solves the problem using the Vampire theorem prover.

This method consumes the problem and invokes Vampire to either prove the conjecture from the axioms, find a counterexample, or determine that the result is unknown.

Returns

A ProofRes indicating whether the conjecture was proved, found to be unprovable, or whether the result is unknown (due to timeout, memory limits, or incompleteness).

Examples

use vampire_prover::{Function, Predicate, Problem, ProofRes, Options, forall};

let p = Predicate::new("P", 1);
let x = Function::constant("x");

let result = Problem::new(Options::new())
    .with_axiom(p.with(x))
    .conjecture(p.with(x))
    .solve();

assert_eq!(result, ProofRes::Proved);

Examples found in repository

examples/name_reuse.rs (line 22)

fn main() {
    let x1 = Function::new("x", 0);
    let x2 = Function::new("x", 0);

    dbg!(x1, x2);
    dbg!(x1 == x2);

    let y1 = Function::new("y", 0);
    let y2 = Function::new("y", 1);

    dbg!(y1, y2);

    let z1 = Function::new("z", 0);
    let z2 = Predicate::new("z", 0);

    dbg!(z1, z2);

    let solution = Problem::new(Options::new())
        .with_axiom(y1.with(&[]).eq(y2.with(&[y1.with(&[])])))
        .solve();

    dbg!(solution);
}

examples/bench_index2.rs (line 176)

fn run_proof(i: usize) -> ProofRes {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new(&format!("mult{i}"), 2);
    let inv = Function::new(&format!("inv{i}"), 1);
    let one = Function::constant(&format!("1{i}"));

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with(&[x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(&[x]);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(&[one]);

    // And is closed under multiplication
    let h_mul_closed =
        forall(|x| forall(|y| (h.with(&[x]) & h.with(&[y])) >> h.with(&[mul(x, y)])));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(&[x]) >> h.with(&[inv.with(&[x])]));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(&[x]);
        // but everything is in H or x H
        let class = forall(|y| h.with(&[y]) | h.with(&[mul(inv.with(&[x]), y)]));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(&[x]);
        let conj_x = forall(|y| {
            let y_inv = inv.with(&[y]);
            h.with(&[mul(mul(y, x), y_inv)])
        });
        h_x.iff(conj_x)
    });

    Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve()
}

pub fn solve_and_prove(&mut self) -> (ProofRes, Option<Proof>)

Solves the problem and, if proved, returns the proof.

This is like Problem::solve but also extracts a Proof when the conjecture is successfully proved. If the result is anything other than ProofRes::Proved, the second element of the tuple is None.

Returns

A tuple of (ProofRes, Option<Proof>). The Option<Proof> is Some only when the result is ProofRes::Proved.

Examples

use vampire_prover::{Function, Predicate, Problem, ProofRes, Options, forall};

let p = Predicate::new("P", 1);
let x = Function::constant("x");

let (result, proof) = Problem::new(Options::new())
    .with_axiom(p.with(x))
    .conjecture(p.with(x))
    .solve_and_prove();

assert_eq!(result, ProofRes::Proved);
assert!(proof.is_some());
println!("{}", proof.unwrap());

Examples found in repository

examples/group.rs (line 38)

fn main() {
    // Prove that the identity element works on the left using group axioms
    // In group theory, if we define a group with:
    //   - Right identity: x * 1 = x
    //   - Right inverse: x * inv(x) = 1
    //   - Associativity: (x * y) * z = x * (y * z)
    // Then we can prove the left identity: 1 * x = x

    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Conjecture: Left identity - ∀x. 1 * x = x
    let left_identity = forall(|x| mul(one, x).eq(x));

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .conjecture(left_identity)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

examples/group2.rs (line 65)

fn main() {
    // Prove that every subgroup of index 2 is normal.
    let mult = Function::new("mult", 2);
    let inv = Function::new("inv", 1);
    let one = Function::constant("1");

    // Helper to make multiplication more readable
    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };

    // Group Axiom 1: Right identity - ∀x. x * 1 = x
    let right_identity = forall(|x| mul(x, one).eq(x));

    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
    let right_inverse = forall(|x| {
        let inv_x = inv.with(x);
        mul(x, inv_x).eq(one)
    });

    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));

    // Describe the subgroup
    let h = Predicate::new("h", 1);

    // Any subgroup contains the identity
    let h_ident = h.with(one);

    // And is closed under multiplication
    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));

    // And is closed under inverse
    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));

    // H specifically is of order 2
    let h_index_2 = exists(|x| {
        // an element not in H
        let not_in_h = !h.with(x);
        // but everything is in H or x H
        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));

        not_in_h & class
    });

    // Conjecture: H is normal
    let h_normal = forall(|x| {
        let h_x = h.with(x);
        let conj_x = forall(|y| {
            let y_inv = inv.with(y);
            h.with(mul(mul(y, x), y_inv))
        });
        h_x.iff(conj_x)
    });

    let (solution, proof) = Problem::new(Options::new())
        .with_axiom(right_identity)
        .with_axiom(right_inverse)
        .with_axiom(associativity)
        .with_axiom(h_ident)
        .with_axiom(h_mul_closed)
        .with_axiom(h_inv_closed)
        .with_axiom(h_index_2)
        .conjecture(h_normal)
        .solve_and_prove();

    if let Some(proof) = proof {
        println!("{}", proof);
    }

    assert_eq!(solution, ProofRes::Proved);
}

Trait Implementations

impl Clone for Problem

fn clone(&self) -> Problem

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Problem

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.