TY - GEN
T1 - Focusing and polarization in intuitionistic logic
AU - Liang, Chuck
AU - Miller, Dale
PY - 2007/1/1
Y1 - 2007/1/1
N2 - A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof search and the proof normalization approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree or another. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems.
AB - A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof search and the proof normalization approaches to computation. Various proof systems in literature exhibit characteristics of focusing to one degree or another. We present a new, focused proof system for intuitionistic logic, called LJF, and show how other proof systems can be mapped into the new system by inserting logical connectives that prematurely stop focusing. We also use LJF to design a focused proof system for classical logic. Our approach to the design and analysis of these systems is based on the completeness of focusing in linear logic and on the notion of polarity that appears in Girard's LC and LU proof systems.
UR - https://www.scopus.com/pages/publications/38049023971
U2 - 10.1007/978-3-540-74915-8_34
DO - 10.1007/978-3-540-74915-8_34
M3 - Conference contribution
AN - SCOPUS:38049023971
SN - 9783540749141
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 451
EP - 465
BT - Computer Science Logic - 21st International Workshop, CSL 2007 and 16th Annual Conference of the EACSL, Proceedings
PB - Springer Verlag
T2 - 21st International Workshop on Computer Science Logic, CSL 2007 and 16th Annual Conference of the European Association for Computer Science Logic, EACSL
Y2 - 11 September 2007 through 15 September 2007
ER -