Struct Formula 

pub struct Formula { /* private fields */ }

A formula in first-order logic.

Formulas are logical statements that can be true or false. They include:

• Atomic formulas: predicates and equalities
• Logical connectives: AND (&), OR (|), NOT (!), implication (>>), biconditional
• Quantifiers: universal (∀) and existential (∃)

Examples

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

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

// Atomic formula
let px = p.with(x);
let qx = q.with(x);

// Conjunction: P(x) ∧ Q(x)
let both = px & qx;

// Disjunction: P(x) ∨ Q(x)
let either = px | qx;

// Implication: P(x) → Q(x)
let implies = px >> qx;

// Negation: ¬P(x)
let not_px = !px;

// Universal quantification: ∀x. P(x)
let all = forall(|x| p.with(x));

Implementations

impl Formula

pub fn to_string(&self) -> String

Converts this formula to a string representation.

Panics

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

Examples

use vampire_prover::{Function, Predicate};

let p = Predicate::new("P", 1);
let x = Function::constant("x");
let formula = p.with(x);
println!("{}", formula.to_string()); // Prints the vampire string representation

pub fn new_predicate(pred: Predicate, args: &[Term]) -> Self

Creates an atomic formula by applying a predicate to arguments.

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

Panics

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

Examples

use vampire_prover::{Function, Predicate, Formula};

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

let formula = Formula::new_predicate(mortal, &[socrates]);

pub fn new_eq(lhs: Term, rhs: Term) -> Self

Creates an equality formula between two terms.

This is typically called via Term::eq rather than directly.

Examples

use vampire_prover::{Function, Formula};

let x = Function::constant("x");
let y = Function::constant("y");

let eq = Formula::new_eq(x, y);

pub fn new_and(formulas: &[Formula]) -> Self

Creates a conjunction (AND) of multiple formulas.

For two formulas, the & operator is more convenient.

Examples

use vampire_prover::{Function, Predicate, Formula};

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

// P(x) ∧ Q(x) ∧ R(x)
let all_three = Formula::new_and(&[
    p.with(x),
    q.with(x),
    r.with(x),
]);

pub fn new_or(formulas: &[Formula]) -> Self

Creates a disjunction (OR) of multiple formulas.

For two formulas, the | operator is more convenient.

Examples

use vampire_prover::{Function, Predicate, Formula};

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

// P(x) ∨ Q(x) ∨ R(x)
let any = Formula::new_or(&[
    p.with(x),
    q.with(x),
    r.with(x),
]);

pub fn new_not(formula: Formula) -> Self

Creates a negation (NOT) of a formula.

The ! operator is more convenient than calling this directly.

Examples

use vampire_prover::{Function, Predicate, Formula};

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

let not_p = Formula::new_not(p.with(x));

pub fn new_true() -> Self

Creates the true (tautology) formula.

Examples

use vampire_prover::Formula;

let t = Formula::new_true();

pub fn new_false() -> Self

Creates the false (contradiction) formula.

Examples

use vampire_prover::Formula;

let f = Formula::new_false();

pub fn new_forall(var: u32, f: Formula) -> Self

Creates a universally quantified formula.

The forall helper function provides a more ergonomic interface.

Arguments

• var - The index of the variable to quantify
• f - The formula body

Examples

use vampire_prover::{Function, Predicate, Formula, Term};

let p = Predicate::new("P", 1);
let x = Term::new_var(0);

// ∀x. P(x)
let all_p = Formula::new_forall(0, p.with(x));

pub fn new_exists(var: u32, f: Formula) -> Self

Creates an existentially quantified formula.

The exists helper function provides a more ergonomic interface.

Arguments

• var - The index of the variable to quantify
• f - The formula body

Examples

use vampire_prover::{Function, Predicate, Formula, Term};

let p = Predicate::new("P", 1);
let x = Term::new_var(0);

// ∃x. P(x)
let some_p = Formula::new_exists(0, p.with(x));

pub fn imp(&self, rhs: Formula) -> Self

Creates an implication from this formula to another.

The >> operator is more convenient than calling this directly.

Arguments

• rhs - The consequent (right-hand side) of the implication

Examples

use vampire_prover::{Function, Predicate};

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

// P(x) → Q(x)
let implication = p.with(x).imp(q.with(x));

pub fn iff(&self, rhs: Formula) -> Self

Creates a biconditional (if and only if) between this formula and another.

A biconditional P ↔ Q is true when both formulas have the same truth value.

Arguments

• rhs - The right-hand side of the biconditional

Examples

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

let even = Predicate::new("even", 1);
let div_by_2 = Predicate::new("divisible_by_2", 1);

// ∀x. even(x) ↔ divisible_by_2(x)
let equiv = forall(|x| {
    even.with(x).iff(div_by_2.with(x))
});

Examples found in repository

examples/bench_index2.rs (line 164)

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 53)

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 BitAnd for Formula

Implements the & operator for conjunction (AND).

Examples

use vampire_prover::{Function, Predicate};

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

// P(x) ∧ Q(x)
let both = p.with(x) & q.with(x);

type Output = Formula

The resulting type after applying the & operator.

fn bitand(self, rhs: Self) -> Self::Output

Performs the & operation.

impl BitOr for Formula

Implements the | operator for disjunction (OR).

Examples

use vampire_prover::{Function, Predicate};

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

// P(x) ∨ Q(x)
let either = p.with(x) | q.with(x);

type Output = Formula

The resulting type after applying the | operator.

fn bitor(self, rhs: Self) -> Self::Output

Performs the | operation.

impl Clone for Formula

fn clone(&self) -> Formula

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Formula

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

Formats the value using the given formatter.

impl Display for Formula

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

Formats the value using the given formatter.

impl Hash for Formula

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Not for Formula

Implements the ! operator for negation (NOT).

Examples

use vampire_prover::{Function, Predicate};

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

// ¬P(x)
let not_p = !p.with(x);

type Output = Formula

The resulting type after applying the ! operator.

fn not(self) -> Self::Output

Performs the unary ! operation.

impl PartialEq for Formula

fn eq(&self, other: &Self) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Shr for Formula

Implements the >> operator for implication.

Examples

use vampire_prover::{Function, Predicate};

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

// P(x) → Q(x)
let implies = p.with(x) >> q.with(x);

type Output = Formula

The resulting type after applying the >> operator.

fn shr(self, rhs: Self) -> Self::Output

Performs the >> operation.

impl Copy for Formula

impl Eq for Formula