Focusing and Polarization in Intuitionistic Logic

Chuck Liang 1 Dale Miller 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 that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof search and the proof normalization approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree or another. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other 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 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 :
Communication dans un congrès
Computer Science Logic, Sep 2007, Lausanne, Switzerland
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00167231
Contributeur : Dale Miller <>
Soumis le : jeudi 16 août 2007 - 19:19:32
Dernière modification le : jeudi 9 février 2017 - 15:16:03
Document(s) archivé(s) le : jeudi 8 avril 2010 - 21:19:08

Fichiers

csl07-014.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

  • HAL Id : inria-00167231, version 1
  • ARXIV : 0708.2252

Collections

Citation

Chuck Liang, Dale Miller. Focusing and Polarization in Intuitionistic Logic. Computer Science Logic, Sep 2007, Lausanne, Switzerland. 〈inria-00167231〉

Partager

Métriques

Consultations de la notice

380

Téléchargements de fichiers

203