Focusing is a proof-theoretic device to structure proof search in the sequent calculus: it provides a normal form to cut-free proofs in which the application of invertible and non-invertible inference rules is structured in two separate and disjoint phases. It is commonly believed that every “reasonable” sequent calculus has a natural focused version. Although stemming from proof-search considerations, focusing has not been thoroughly investigated in actual theorem proving, in par- ticular w.r.t. termination, if not for the folk observations that only neg- ative formulas need to be duplicated (or contracted if seen from the top down) in the focusing phase. We present a contraction-free (and hence terminating) focused proof system for multi-succedent propositional intu- itionistic logic, which refines the G4ip calculus of Vorob’ev, Hudelmeier and Dyckhoff. We prove the completeness of the approach semantically and argue that this offers a viable alternative to other more syntactical means.
Avellone, A., Fiorentini, C., & Momigliano, A. (2013). Focusing on Contraction. In Proceedings of the 28th Italian Conference on Computational Logic. Catania, Italy, September 25-27, 2013 (pp.65-81).
|Citazione:||Avellone, A., Fiorentini, C., & Momigliano, A. (2013). Focusing on Contraction. In Proceedings of the 28th Italian Conference on Computational Logic. Catania, Italy, September 25-27, 2013 (pp.65-81).|
|Carattere della pubblicazione:||Scientifica|
|Presenza di un coautore afferente ad Istituzioni straniere:||No|
|Titolo:||Focusing on Contraction|
|Autori:||Avellone, A; Fiorentini, C; Momigliano, A|
|Data di pubblicazione:||2013|
|Nome del convegno:||Italian Conference on Computational Logic|
|Serie:||CEUR WORKSHOP PROCEEDINGS|
|Appare nelle tipologie:||02 - Intervento a convegno|