Struct Sequent 

pub struct Sequent {
    pub antecedents: Vec<TLExpr>,
    pub consequents: Vec<TLExpr>,
}

A sequent is a formal statement Γ ⊢ Δ representing an entailment relation.

• antecedents (Γ): Multiset of hypothesis formulas (left side)
• consequents (Δ): Multiset of conclusion formulas (right side)

The sequent is valid if: assuming all antecedents are true, at least one consequent must be true.

Fields

antecedents: Vec<TLExpr>

Hypothesis formulas (left side of ⊢)

consequents: Vec<TLExpr>

Conclusion formulas (right side of ⊢)

Implementations

impl Sequent

pub fn new(antecedents: Vec<TLExpr>, consequents: Vec<TLExpr>) -> Self

Create a new sequent from antecedents and consequents.

pub fn identity(formula: TLExpr) -> Self

Create an identity sequent: A ⊢ A

pub fn is_axiom(&self) -> bool

Check if this is an axiom (identity sequent where some antecedent equals some consequent).

pub fn weaken_left(self, formula: TLExpr) -> Self

Apply weakening rule: add a formula to antecedents.

pub fn weaken_right(self, formula: TLExpr) -> Self

Apply weakening rule: add a formula to consequents.

pub fn contract_left(self, index: usize) -> Option<Self>

Apply contraction rule: remove duplicate from antecedents.

pub fn contract_right(self, index: usize) -> Option<Self>

Apply contraction rule: remove duplicate from consequents.

pub fn free_vars(&self) -> HashSet<String>

Get all free variables in the sequent.

pub fn substitute(&self, var: &str, term: &Term) -> Self

Substitute a term for a variable throughout the sequent.

This creates a new substitution and applies it to all formulas in the sequent. The substitution is capture-avoiding for bound variables in quantifiers.

Example

use tensorlogic_ir::{Sequent, TLExpr, Term};

// P(x) ⊢ P(x)
let p_x = TLExpr::pred("P", vec![Term::var("x")]);
let seq = Sequent::identity(p_x);

// Substitute x with a
let seq_subst = seq.substitute("x", &Term::constant("a"));

// Result should be P(a) ⊢ P(a)

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.

impl<'de> Deserialize<'de> for Sequent

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Sequent

fn eq(&self, other: &Sequent) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for Sequent

fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl StructuralPartialEq for Sequent