TY - GEN
T1 - From proofs to focused proofs
T2 - 21st International Workshop on Computer Science Logic, CSL 2007 and 16th Annual Conference of the European Association for Computer Science Logic, EACSL
AU - Miller, Dale
AU - Saurin, Alexis
PY - 2007/1/1
Y1 - 2007/1/1
N2 - Probably the most significant result concerning cut-free sequent calculus proofs in linear logic is the completeness of focused proofs. This completeness theorem has a number of proof theoretic applications - e.g. in game semantics, Ludics, and proof search -and more computer science applications - e.g. logic programming, call-by-name/value evaluation. Andreoli proved this theorem for first-order linear logic 15 years ago. In the present paper, we give a new proof of the completeness of focused proofs in terms of proof transformation. The proof of this theorem is simple and modular: it is first proved for MALL and then is extended to full linear logic. Given its modular structure, we show how the proof can be extended to larger systems, such as logics with induction. Our analysis of focused proofs will employ a proof transformation method that leads us to study how focusing and cut elimination interact. A key component of our proof is the construction of a focalization graph which provides an abstraction over how focusing can be organized within a given cut-free proof. Using this graph abstraction allows us to provide a detailed study of atomic bias assignment in a way more refined that is given in Andreoli's original proof. Permitting more flexible assignment of bias will allow this completeness theorem to help establish the completeness of a number of other automated deduction procedures. Focalization graphs can be used to justify the introduction of an inference rule for multifocus derivation: a rule that should help us better understand the relations between sequentiality and concurrency in linear logic.
AB - Probably the most significant result concerning cut-free sequent calculus proofs in linear logic is the completeness of focused proofs. This completeness theorem has a number of proof theoretic applications - e.g. in game semantics, Ludics, and proof search -and more computer science applications - e.g. logic programming, call-by-name/value evaluation. Andreoli proved this theorem for first-order linear logic 15 years ago. In the present paper, we give a new proof of the completeness of focused proofs in terms of proof transformation. The proof of this theorem is simple and modular: it is first proved for MALL and then is extended to full linear logic. Given its modular structure, we show how the proof can be extended to larger systems, such as logics with induction. Our analysis of focused proofs will employ a proof transformation method that leads us to study how focusing and cut elimination interact. A key component of our proof is the construction of a focalization graph which provides an abstraction over how focusing can be organized within a given cut-free proof. Using this graph abstraction allows us to provide a detailed study of atomic bias assignment in a way more refined that is given in Andreoli's original proof. Permitting more flexible assignment of bias will allow this completeness theorem to help establish the completeness of a number of other automated deduction procedures. Focalization graphs can be used to justify the introduction of an inference rule for multifocus derivation: a rule that should help us better understand the relations between sequentiality and concurrency in linear logic.
U2 - 10.1007/978-3-540-74915-8_31
DO - 10.1007/978-3-540-74915-8_31
M3 - Conference contribution
AN - SCOPUS:38049005898
SN - 9783540749141
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 405
EP - 419
BT - Computer Science Logic - 21st International Workshop, CSL 2007 and 16th Annual Conference of the EACSL, Proceedings
PB - Springer Verlag
Y2 - 11 September 2007 through 15 September 2007
ER -