From Axioms to Analytic Rules in Nonclassical Logics

We introduce a systematic procedure to transform large classes of (Hilbert) axioms into equivalent inference rules in sequent and hypersequent calculi. This allows for the automated generation of analytic calculi for a wide range of propositional nonclassical logics including intermediate, fuzzy and substructural logics. Our work encompasses many existing results, allows for the definition of new calculi and contains a uniform semantic proof of cutelimination for hypersequent calculi.

• Type: Conference
• Year: 2008
• Where: LICS
• Authors: Agata Ciabattoni, Nikolaos Galatos, Kazushige Terui
• Keywords: Analytic Calculi, Computer Science, Hypersequent Calculi, LICS 2008, Propositional Nonclassical Logics