Struct CutElimination 

pub struct CutElimination;

Cut elimination transformation.

Cut elimination is a fundamental property of sequent calculus stating that any proof using the cut rule can be transformed into a cut-free proof. This is important for proof normalization and extracting computational content.

Implementations

impl CutElimination

pub fn eliminate(proof: ProofTree) -> ProofTree

Attempt to eliminate all cut rules from a proof tree.

Returns a cut-free proof if successful, or the original proof if cut elimination fails or is not applicable.

pub fn is_cut_free(proof: &ProofTree) -> bool

Check if a proof is cut-free.