Skip to Main content Skip to Navigation
Journal articles

A Focused Approach to Combining Logics

Abstract : We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative-additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut elimination holds in such fragments. From cut elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. We examine certain circumstances, for example, in which a classical lemma can be used in an intuitionistic proof while preserving intuitionistic provability. We also examine the possibility of defining classical-linear hybrid logics.
Document type :
Journal articles
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00772736
Contributor : Dale Miller <>
Submitted on : Friday, January 11, 2013 - 9:34:41 AM
Last modification on : Thursday, January 7, 2021 - 3:40:14 PM
Long-term archiving on: : Friday, April 12, 2013 - 11:16:48 AM

File

lku.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Chuck Liang, Dale Miller. A Focused Approach to Combining Logics. Annals of Pure and Applied Logic, Elsevier Masson, 2011, ⟨10.1016/j.apal.2011.01.012⟩. ⟨hal-00772736⟩

Share

Metrics

Record views

451

Files downloads

424