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 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_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))
});

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 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: &Formula) -> 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

impl StructuralPartialEq for Formula