A Unified Sequent Calculus for Focused Proofs - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

A Unified Sequent Calculus for Focused Proofs

Résumé

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.
Fichier non déposé

Dates et versions

hal-00772347 , version 1 (10-01-2013)

Identifiants

  • HAL Id : hal-00772347 , version 1

Citer

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. ⟨hal-00772347⟩
187 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More