A Focused Approach to Combining Logics

Chuck Liang 1 Dale Miller 2, 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 : We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut elimination holds in such fragments. From cut elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.
Type de document :
Article dans une revue
Annals of Pure and Applied Logic, Elsevier Masson, 2011, 〈10.1016/j.apal.2011.01.012〉
Liste complète des métadonnées

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

Contributeur : Dale Miller <>
Soumis le : vendredi 11 janvier 2013 - 09:34:41
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : vendredi 12 avril 2013 - 11:16:48


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




Chuck Liang, Dale Miller. A Focused Approach to Combining Logics. Annals of Pure and Applied Logic, Elsevier Masson, 2011, 〈10.1016/j.apal.2011.01.012〉. 〈hal-00772736〉



Consultations de la notice


Téléchargements de fichiers