Struct ProofNet 

pub struct ProofNet {
    pub formulas: Vec<LinearFormula>,
    pub links: Vec<(usize, usize)>,
}

A proof net: a list of formulas (formula occurrences) with axiom/cut links.

Fields

formulas: Vec<LinearFormula>

The formulas (conclusions) of the proof net.

links: Vec<(usize, usize)>

Links: pairs of formula occurrence indices connected by axiom or cut.

Implementations

impl ProofNet

pub fn new(formulas: Vec<LinearFormula>) -> Self

Create a new proof net with the given formulas and no links.

pub fn add_link(&mut self, i: usize, j: usize)

Add a link between formula occurrences i and j.

pub fn is_well_typed(&self) -> bool

Check if the proof net is well-typed: every formula occurrence appears in exactly one link.

pub fn correctness_criterion_danos_regnier(&self) -> bool

Danos-Regnier correctness criterion: removing any subset of par-links leaves a connected acyclic graph.

This is a simplified check: we verify the axiom links form a perfect matching and the graph is connected (full DR requires switching).

pub fn size(&self) -> usize

Number of formula occurrences.

Trait Implementations

impl Clone for ProofNet

fn clone(&self) -> ProofNet

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofNet

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

Formats the value using the given formatter.