Struct Sequent 

pub struct Sequent {
    pub antecedent: Vec<NnfFormula>,
    pub succedent: Vec<NnfFormula>,
}

A sequent in propositional sequent calculus (LK/LJ).

A sequent Γ ⊢ Δ consists of a context (antecedent) and a conclusion (succedent). For LJ (intuitionistic), Δ has at most one formula.

Fields

antecedent: Vec<NnfFormula>

Antecedent: list of assumption formulas.

succedent: Vec<NnfFormula>

Succedent: list of conclusion formulas (at most one for intuitionistic).

Implementations

impl Sequent

pub fn empty() -> Self

Create an empty sequent ⊢ .

pub fn new(antecedent: Vec<NnfFormula>, succedent: Vec<NnfFormula>) -> Self

Create a sequent from antecedent and succedent.

pub fn axiom(p: NnfFormula) -> Self

Create an axiom sequent: p ⊢ p.

pub fn is_initial(&self) -> bool

Check if this is an initial sequent (antecedent and succedent share a formula).

pub fn is_classically_valid(&self, num_vars: usize) -> bool

Check if this sequent is classically valid (all atoms satisfied under any assignment).

pub fn size(&self) -> usize

Number of formulas in the sequent.

pub fn with_assumption(self, f: NnfFormula) -> Self

Add a formula to the antecedent.

pub fn with_conclusion(self, f: NnfFormula) -> Self

Add a formula to the succedent.

pub fn has_false_in_antecedent(&self) -> bool

Check if the antecedent contains Bot (False), making the sequent trivially valid.

pub fn has_true_in_succedent(&self) -> bool

Check if the succedent contains Top (True), making the sequent trivially valid.

Trait Implementations

impl Clone for Sequent

fn clone(&self) -> Sequent

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Sequent

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

Formats the value using the given formatter.