Expanding the Realm of Systematic Proof Theory

Agata Ciabattoni 1 Lutz Straßburger 2 Kazushige Terui 3
2 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : This paper is part of a general project of developing a sys- tematic and algebraic proof theory for nonclassical logics. Generaliz- ing our previous work on intuitionistic-substructural axioms and single- conclusion (hyper)sequent calculi, we define a hierarchy on Hilbert ax- ioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level P3 of the hierarchy into inference rules in multiple-conclusion (hy- per)sequent calculi, which enjoy cut-elimination under a certain con- dition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than P3 . The case study of Abelian and Lukasiewicz logic is outlined.
Type de document :
Communication dans un congrès
Computer Science Logic, CSL'09, 2009, Coimbra, Portugal. 2009, 〈10.1007/978-3-642-04027-6_14〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

Contributeur : Lutz Straßburger <>
Soumis le : vendredi 30 novembre 2012 - 11:27:08
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : vendredi 1 mars 2013 - 02:30:10


Fichiers produits par l'(les) auteur(s)




Agata Ciabattoni, Lutz Straßburger, Kazushige Terui. Expanding the Realm of Systematic Proof Theory. Computer Science Logic, CSL'09, 2009, Coimbra, Portugal. 2009, 〈10.1007/978-3-642-04027-6_14〉. 〈inria-00436420〉



Consultations de la notice


Téléchargements de fichiers