@inproceedings{79bd71dd972a4ce9b54a2cf6df175982,
title = "A unified sequent calculus for focused proofs",
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.",
keywords = "Focused proof systems, Linear logic, Proof theory",
author = "Chuck Liang and Dale Miller",
year = "2009",
month = nov,
day = "6",
doi = "10.1109/LICS.2009.47",
language = "English",
isbn = "9780769537467",
series = "Proceedings - Symposium on Logic in Computer Science",
pages = "355--364",
booktitle = "Proceedings - 2009 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009",
note = "2009 24th Annual IEEE Symposium on Logic In Computer Science, LICS 2009 ; Conference date: 11-08-2009 Through 14-08-2009",
}