Logic in Computer Science, Symposium on (2008)
June 24, 2008 to June 27, 2008
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2008.39
We introduce a systematic procedure to transform large classesof (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 cut-elimination for hypersequent calculi.
nonclassical logics, sequent calculi, hypersequent calculi, semantic cut-elimination
A. Ciabattoni, N. Galatos and K. Terui, "From Axioms to Analytic Rules in Nonclassical Logics," 23rd Annual IEEE Symposium on Logic in Computer Science (LICS 2008)(LICS), Pittsburgh, PA, 2008, pp. 229-240.