Struct Proof 

pub struct Proof { /* private fields */ }

A proof produced by the Vampire theorem prover.

A Proof is a sequence of ProofSteps that together form a complete derivation of a contradiction from the negated conjecture and axioms. Each step records the inference rule used and the indices of the premises (earlier steps) it was derived from.

Proofs are obtained via Problem::solve_and_prove.

Display

Proof implements std::fmt::Display, which prints each step on its own line in the format <index>: <conclusion> [<rule> <premise-indices>].

Examples

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

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

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

if let Some(proof) = proof {
    for step in proof.steps() {
        println!("{}: {:?}", step.discovery_order(), step.rule());
    }
}

Implementations

impl Proof

pub fn steps(&self) -> &[ProofStep]

Returns all proof steps in the order Vampire discovered them.

Steps are sorted by their ProofStep::discovery_order. Because each step’s premises always have a lower discovery order than the step itself, this ordering is also a valid topological ordering of the proof DAG.

pub fn topo_iter(&self) -> impl Iterator<Item = &ProofStep>

Iterates over proof steps in topological order (discovery order).

This is equivalent to iterating over Proof::steps and is provided for clarity when the topological property matters.

Trait Implementations

impl Clone for Proof

fn clone(&self) -> Proof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Proof

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

Formats the value using the given formatter.

impl Display for Proof

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

Formats the value using the given formatter.

impl Index<usize> for Proof

type Output = ProofStep

The returned type after indexing.

fn index(&self, index: usize) -> &Self::Output

Performs the indexing (container[index]) operation.

impl PartialEq for Proof

fn eq(&self, other: &Proof) -> 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 Eq for Proof

impl StructuralPartialEq for Proof