Sciweavers

Share
CSL
2007
Springer

From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic

9 years 2 months ago
From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
Abstract. 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 focalizat...
Dale Miller, Alexis Saurin
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CSL
Authors Dale Miller, Alexis Saurin
Comments (0)
books