Struct ProofTree 

pub struct ProofTree {
    pub conclusion: Sequent,
    pub rule: InferenceRule,
    pub premises: Vec<ProofTree>,
}

A proof tree in sequent calculus.

Represents a derivation tree showing how a sequent is proved using inference rules applied to premises.

Fields

conclusion: Sequent

The conclusion sequent of this proof step

rule: InferenceRule

The inference rule applied

premises: Vec<ProofTree>

Premise proof trees (subproofs)

Implementations

impl ProofTree

pub fn identity(formula: TLExpr) -> Self

Create a proof tree for an identity axiom.

pub fn new( conclusion: Sequent, rule: InferenceRule, premises: Vec<ProofTree>, ) -> Self

Create a proof tree with premises and rule.

pub fn is_valid(&self) -> bool

Check if this proof tree is valid (premises correctly derive conclusion).

pub fn depth(&self) -> usize

Get the depth of this proof tree.

pub fn size(&self) -> usize

Count the number of inference rule applications in this proof.

pub fn uses_cut(&self) -> bool

Check if this proof uses the cut rule.

Trait Implementations

impl Clone for ProofTree

fn clone(&self) -> ProofTree

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofTree

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

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for ProofTree

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for ProofTree

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

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for ProofTree