Module sequent 

Sequent Calculus for Proof-Theoretic Foundations

This module implements sequent calculus representations and inference rules for TensorLogic. Sequent calculus provides a formal foundation for logical reasoning and proof construction.

Overview

A sequent is a formal statement of the form Γ ⊢ Δ where:

• Γ (Gamma) is a multiset of antecedent formulas (hypotheses)
• Δ (Delta) is a multiset of consequent formulas (conclusions)
• ⊢ (turnstile) represents the entailment relation

The sequent Γ ⊢ Δ is valid if: assuming all formulas in Γ are true, at least one formula in Δ must be true.

Inference Rules

This module implements the following sequent calculus rules:

Structural Rules

• Identity: A ⊢ A
• Weakening: From Γ ⊢ Δ derive Γ, A ⊢ Δ or Γ ⊢ Δ, A
• Contraction: From Γ, A, A ⊢ Δ derive Γ, A ⊢ Δ
• Exchange: Reorder formulas in Γ or Δ
• Cut: From Γ ⊢ Δ, A and A, Γ' ⊢ Δ' derive Γ, Γ' ⊢ Δ, Δ'

Logical Rules (Left and Right)

• AND-Left: From Γ, A, B ⊢ Δ derive Γ, A ∧ B ⊢ Δ
• AND-Right: From Γ ⊢ Δ, A and Γ ⊢ Δ, B derive Γ ⊢ Δ, A ∧ B
• OR-Left: From Γ, A ⊢ Δ and Γ, B ⊢ Δ derive Γ, A ∨ B ⊢ Δ
• OR-Right: From Γ ⊢ Δ, A, B derive Γ ⊢ Δ, A ∨ B
• NOT-Left: From Γ ⊢ Δ, A derive Γ, ¬A ⊢ Δ
• NOT-Right: From Γ, A ⊢ Δ derive Γ ⊢ Δ, ¬A
• IMPLY-Left: From Γ ⊢ Δ, A and Γ, B ⊢ Δ derive Γ, A → B ⊢ Δ
• IMPLY-Right: From Γ, A ⊢ Δ, B derive Γ ⊢ Δ, A → B

Quantifier Rules

• EXISTS-Left: From Γ, A[t/x] ⊢ Δ derive Γ, ∃x.A ⊢ Δ (t is fresh)
• EXISTS-Right: From Γ ⊢ Δ, A[t/x] derive Γ ⊢ Δ, ∃x.A
• FORALL-Left: From Γ, A[t/x] ⊢ Δ derive Γ, ∀x.A ⊢ Δ
• FORALL-Right: From Γ ⊢ Δ, A[t/x] derive Γ ⊢ Δ, ∀x.A (t is fresh)

Applications

• Proof Search: Construct proofs by applying inference rules backward
• Proof Checking: Verify that a derivation tree is valid
• Proof Normalization: Transform proofs to normal forms (cut-elimination)
• Compilation: Use sequent calculus to guide tensor compilation strategies

Example

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

// Construct a sequent: P(x) ∧ Q(x) ⊢ P(x)
let p = TLExpr::pred("P", vec![Term::var("x")]);
let q = TLExpr::pred("Q", vec![Term::var("x")]);
let and_pq = TLExpr::and(p.clone(), q);

let conclusion = Sequent::new(vec![and_pq], vec![p.clone()]);

// Construct a proof tree: Identity axiom as premise, then apply AndLeft
let identity_premise = ProofTree::identity(p.clone());
let proof = ProofTree::new(
    conclusion,
    InferenceRule::AndLeft { index: 0 },
    vec![identity_premise]
);

assert!(proof.is_valid());

Structs

CutElimination

Cut elimination transformation.

ProofSearchEngine

Proof search engine for automated theorem proving.

ProofSearchStats

Statistics about proof search.

ProofTree

A proof tree in sequent calculus.

Sequent

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

Enums

InferenceRule

Inference rules in sequent calculus.

ProofSearchStrategy

Proof search strategies for automated theorem proving.