A Unified Sequent Calculus for Focused Proofs

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, X - École polytechnique, 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 logic, intuitionistic logic, and multiplicative-additive linear logic are derived as fragments of LKU by increasing the sensitivity of specialized structural rules to polarity information. We develop a unified, streamlined framework for proving cut-elimination in the various fragments. Furthermore, each sublogic can interact with other fragments through cut. We also consider the possibility of introducing classical-linear hybrid logics.
Type de document :
Communication dans un congrès
LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00772347
Contributeur : Dale Miller <>
Soumis le : jeudi 10 janvier 2013 - 13:38:03
Dernière modification le : jeudi 10 mai 2018 - 02:06:19

Identifiants

  • HAL Id : hal-00772347, version 1

Collections

Citation

Liang Chuck, Dale Miller. A Unified Sequent Calculus for Focused Proofs. LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States. 2009. 〈hal-00772347〉

Partager

Métriques

Consultations de la notice

204