Automated Generation of Analytic Calculi for Logics with Linearity

Abstract. We show how to automatically generate analytic hypersequent calculi for a large class of logics containing the linearity axiom (lin) (A ⊃ B) ∨ (B ⊃ A) starting from existing (single-conclusion) cut-free sequent calculi for the corresponding logics without (lin). As a corollary, we define an analytic calculus for Strict Monoidal T-norm based Logic SMTL.

• Type: Conference
• Year: 2004
• Where: CSL
• Authors: Agata Ciabattoni
• Keywords: Analytic Hypersequent Calculi, CSL 2004, Cut-free Sequent Calculi, Logic