Struct PropositionalProof 

pub struct PropositionalProof {
    pub system: ProofSystem,
    pub lines: Vec<(String, String)>,
    pub conclusion: String,
}

A propositional proof: a sequence of lines each with a justification.

Fields

system: ProofSystem

The proof system used.

lines: Vec<(String, String)>

Lines: (formula_string, justification_string).

conclusion: String

The conclusion formula.

Implementations

impl PropositionalProof

pub fn new(system: ProofSystem, conclusion: impl Into<String>) -> Self

Create an empty proof in the given system for the given conclusion.

pub fn add_line( &mut self, formula: impl Into<String>, justification: impl Into<String>, )

Add a proof line with a justification.

pub fn measure(&self) -> ProofComplexityMeasure

Return the proof complexity measure.

Trait Implementations

impl Clone for PropositionalProof

fn clone(&self) -> PropositionalProof

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for PropositionalProof

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

Formats the value using the given formatter.