Struct LinearSequent 

pub struct LinearSequent {
    pub context: Vec<String>,
    pub conclusion: String,
}

A one-sided linear sequent ⊢ Γ in linear logic.

Fields

context: Vec<String>

The context: a list of formula names (positive occurrences).

conclusion: String

The conclusion formula name.

Implementations

impl LinearSequent

pub fn new(context: Vec<String>, conclusion: impl Into<String>) -> Self

Create a new linear sequent.

pub fn cut_elimination(&self) -> String

Cut elimination: a sequent derivable with cut is derivable without cut.

Returns a string description of the cut-free derivation.

pub fn is_provable(&self) -> bool

Check if the sequent is provable (simplified heuristic).

pub fn one_sided_form(&self) -> String

Return the one-sided form ⊢ Γ, A.

Trait Implementations

impl Clone for LinearSequent

fn clone(&self) -> LinearSequent

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for LinearSequent

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

Formats the value using the given formatter.