Computer Science – Logic in Computer Science
Scientific paper
2011-09-28
Computer Science
Logic in Computer Science
A Twelf formalization is included and an Agda formalization is available at https://github.com/robsimmons/agda-lib/tree/focali
Scientific paper
Focusing, introduced by Jean-Marc Andreoli in the context of classical linear logic, defines a normal form for sequent calculus derivations that cuts down on the number of possible derivations by eagerly applying invertible rules and grouping sequences of non-invertible rules. A focused sequent calculus is defined relative to some non-focused sequent calculus; focalization is the property that every non-focused derivation can be transformed into a focused derivation. In this paper, we present a focused sequent calculus for propositional intuitionistic logic and prove the focalization property relative to a standard presentation of propositional intuitionistic logic. Compared to existing approaches, the proof is quite concise, depending only on the internal soundness and completeness of the focused logic. In turn, both of these properties can be established (and mechanically verified) by structural induction in the style of Pfenning's structural cut elimination without the need for any tedious and repetitious invertibility lemmas. The proof of cut admissibility for the focused system, which establishes internal soundness, is not particularly novel. The proof of identity expansion, which establishes internal completeness, is the principal contribution of this work.
No associations
LandOfFree
Structural focalization does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Structural focalization, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Structural focalization will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-44186