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/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()
}

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/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()
}

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/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()
}

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()
}

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.