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, X - École polytechnique, 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

https://hal.inria.fr/inria-00436420
Contributeur : Lutz Straßburger <>
Soumis le : vendredi 30 novembre 2012 - 11:27:08
Dernière modification le : jeudi 10 mai 2018 - 02:06:43
Document(s) archivé(s) le : vendredi 1 mars 2013 - 02:30:10

Fichier

realm-finalforcsl.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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〉

Partager

Métriques

Consultations de la notice

257

Téléchargements de fichiers

101