Focusing and Polarization in Linear, Intuitionistic, and Classical Logics

Liang Chuck Dale Miller 1, 2
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 : A focused proof system provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured. Within linear logic, the focused proof system of Andreoli provides an elegant and comprehensive normal form for cut-free proofs. Within intuitionistic and classical logics, there are various different proof systems in the literature that exhibit focusing behavior. These focused proof systems have been applied to both the proof search and the proof normalization approaches to computation. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other intuitionistic proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system LKF for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2009, 410 (46), 〈10.1016/j.tcs.2009.07.041〉
Liste complète des métadonnées
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 13:31:18
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14




Liang Chuck, Dale Miller. Focusing and Polarization in Linear, Intuitionistic, and Classical Logics. Theoretical Computer Science, Elsevier, 2009, 410 (46), 〈10.1016/j.tcs.2009.07.041〉. 〈hal-00772342〉



Consultations de la notice