Paper: From Axioms to Analytic Rules in Nonclassical Logics (at LICS 2008)

Authors: Agata Ciabattoni Nikolaos Galatos Kazushige Terui

Abstract

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.

BibTeX

  @InProceedings{CiabattoniGalatosTe-FromAxiomstoAnalyti,
    author = 	 {Agata Ciabattoni and Nikolaos Galatos and Kazushige Terui},
    title = 	 {From Axioms to Analytic Rules in Nonclassical Logics},
    booktitle =  {Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science (LICS 2008)},
    year =	 {2008},
    month =	 {June}, 
    pages =      {229--240},
    location =   {Pittsburgh, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }