Struct ProofStructure 

pub struct ProofStructure {
    pub n_formulas: usize,
    pub links: Vec<Link>,
}

A proof structure: a set of formula occurrences and links.

Fields

n_formulas: usize

Number of formula occurrences.

links: Vec<Link>

The links (axiom, cut, tensor, par, etc.).

Implementations

impl ProofStructure

pub fn new(n_formulas: usize) -> Self

Create a new empty proof structure with n formula occurrences.

pub fn add_link(&mut self, link: Link)

Add a link to the proof structure.

pub fn is_correct(&self) -> bool

Check the Danos-Regnier correctness criterion (simplified: for MLL axiom nets).

A proof structure is correct iff every switching (choice of one conclusion for each par link) yields a spanning tree of the graph. Here we apply a union-find acyclicity check on the axiom links.

pub fn axiom_count(&self) -> usize

Count axiom links.

pub fn cut_count(&self) -> usize

Count cut links.

Trait Implementations

impl Clone for ProofStructure

fn clone(&self) -> ProofStructure

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofStructure

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

Formats the value using the given formatter.