A Unified Sequent Calculus for Focused Proofs
In: LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE ; https://inria.hal.science/hal-00772347 ; LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States, 2009
Konferenz
Zugriff:
International audience ; 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.
| Titel: |
A Unified Sequent Calculus for Focused Proofs
|
|---|---|
| Autor/in / Beteiligte Person: | Chuck, Liang ; Miller, Dale ; Laboratoire d'informatique de l'École polytechnique Palaiseau (LIX) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS) ; Proof search and reasoning with logic specifications (PARSIFAL) ; École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Link: | |
| Zeitschrift: | LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE ; https://inria.hal.science/hal-00772347 ; LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States, 2009 |
| Veröffentlichung: | HAL CCSD, 2009 |
| Medientyp: | Konferenz |
| Schlagwort: |
|
| Sonstiges: |
|