A Semantical Analysis of Focusing and Contraction in Intuitionistic Logic

• Autorzy: Avellone A. , Fiorentini C. , Momigliano A.

Identyfikatory

DOI

10.3233/FI-2015-1253

• Konferencja: Italian Conference on Computational Logic, CILC 2013, (25-27.09.2013; Catania, Italy)
• Języki publikacji: EN

Abstrakty

EN

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. Although stemming from proofsearch considerations, focusing has not been thoroughly investigated in actual theorem proving, in particular w.r.t. termination. We present a contraction-free (and hence terminating) focused multisuccedent sequent calculus for propositional intuitionistic logic, which refines the G4ip calculus in the tradition of Vorob’ev, Hudelmeier and Dyckhoff. We prove completeness of the calculus semantically and argue that this offers a viable alternative to other more syntactical means.

Słowa kluczowe

EN

mathematical proofs; propositional calculus; intuitionistic mathematics; contraction operator; structural analysis

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 140, nr 3/4
• Strony: 247--262
• Opis fizyczny: Bibliogr. 31 poz.

Twórcy

autor

Avellone A.

• Dipartimenti di Statistica e Metodi Quantitativi Universit`a degli Studi di Milano-Bicocca, Italy

autor

Fiorentini C.

• Dipartimento di Informatica Universit`a degli Studi di Milano, Italy

autor

Momigliano A.

• Dipartimento di Informatica Universit`a degli Studi di Milano, Italy

Bibliografia

• [1] Andreoli, J.-M.: Logic Programming with Focusing Proofs in Linear Logic, J. Log. Comput., 2(3), 1992, 297–347.
• [2] Avellone, A., Ferrari, M., Miglioli, P.: Duplication-Free Tableau Calculi and Related Cut-Free Sequent Calculi for the Interpolable Propositional Intermediate Logics, Logic J. of the IGPL, 7(4), 1999, 447–480.
• [3] Avellone, A., Fiorentini, C., Momigliano, A.: Focusing on Contraction, Proceedings of the 28th Italian Conference on Computational Logic, Catania, Italy, September 25-27, 2013. (D. Cantone, M. N. Asmundo, Eds.), 1068, CEUR-WS.org, 2013.
• [4] Avellone, A., Fiorino, G., Moscato, U.: Optimization Techniques for Propositional Intuitionistic Logic and their Implementation, Theor. Comput. Sci., 409(1), 2008, 41–58.
• [5] Avron, A., Konikowska, B.: Decomposition Proof Systems for G¨odel-Dummett Logics, Studia Logica, 69(2), 2001, 197–219.
• [6] Baelde, D.: Least and Greatest Fixed Points in Linear Logic, ACM Trans. Comput. Logic, 13(1), 2012, 1–44.
• [7] Baelde, D., Miller, D., Snow, Z.: Focused Inductive Theorem Proving, IJCAR (J. Giesl, R. H¨ahnle, Eds.), 6173, Springer, 2010.
• [8] Chaudhuri, K.: The Focused Inverse Method for Linear Logic, Ph.D. Thesis, Carnegie Mellon University, 2006.
• [9] Chaudhuri, K., Pfenning, F., Price, G.: A Logical Characterization of Forward and Backward Chaining in the Inverse Method, J. Autom. Reasoning, 40(2-3), 2008, 133–177.
• [10] Dyckhoff, R.: Contraction-Free Sequent Calculi for Intuitionistic Logic, J. Symb. Log., 57(3), 1992, 795–807.
• [11] Dyckhoff, R., Lengrand, S.: LJQ: a Strongly Focused Calculus for Intuitionistic Logic, Computability in Europe 2006 (A. Beckmann, et al., Eds.), 3988, Springer, 2006.
• [12] Dyckhoff, R., Negri, S.: Admissibility of Structural Rules for Contraction-Free Systems of Intuitionistic Logic, J. Symb. Log., 65(4), 2000, 1499–1518.
• [13] Ferrari, M., Fiorentini, C., Fiorino, G.: Contraction-Free Linear Depth Sequent Calculi for Intuitionistic Propositional Logicwith the Subformula Property andMinimalDepth Counter-Models, J. Autom. Reasoning, 2012, 1–21.
• [14] Ferrari, M., Fiorentini, C., Fiorino, G.: A Terminating Evaluation-Driven Variant of G3i, TABLEAUX (D. Galmiche, D. Larchey-Wendling, Eds.), 8123, Springer, 2013.
• [15] Ferrari, M., Fiorentini, C., Fiorino, G.: An Evaluation-Driven Decision Procedure for G3i, ACM Trans. Comput. Logic, 16(1), 2015, 8:1–8:37.
• [16] Fiorino, G.: Fast Decision Procedure for Propositional Dummett Logic Based on a Multiple Premise Tableau Calculus, Inf. Sci., 180(19), 2010, 3633–3646.
• [17] Gabbay, D., Olivetti, N.: Goal-Directed Proof Theory, vol. 21 of Applied Logic Series, Kluwer Academic Publishers, August 2000.
• [18] Henriksen, A. S.: A Contraction-free Focused Sequent Calculus for Classical Propositional Pogic, April 2011, Leibnitz International Proceedings in Informatics, Daghstul.
• [19] Herbelin, H.: A Lambda-Calculus Structure Isomorphic to Gentzen-Style Sequent Calculus Structure, CSL (L. Pacholski, J. Tiuryn, Eds.), 933, Springer, 1994.
• [20] Howe, J. M.: Proof Search Issues in Some Non-Classical Logics, Ph.D. Thesis, University of St. Andrews, 1998.
• [21] Liang, C., Miller, D.: Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, Theor. Comput. Sci., 410(46), 2009, 4747–4768.
• [22] Liang, C., Miller, D.: Kripke semantics and proof systems for combining intuitionistic logic and classical logic, Ann. Pure Appl. Logic, 164(2), 2013, 86–111.
• [23] Maehara, S.: Eine Darstellung der Intuitionistischen Logik in der Klassischen, Nagoya Mathematical Journal, 1954, 45–64.
• [24] McLaughlin, S., Pfenning, F.: Imogen: Focusing the Polarized InverseMethod for Intuitionistic Propositional Logic, LPAR (I. Cervesato, H. Veith, A. Voronkov, Eds.), 5330, Springer, 2008.
• [25] Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform Proofs as a Foundation for Logic Programming, Annals of Pure and Applied Logic, 51, 1991, 125–157.
• [26] Miller, D., Pimentel, E.: A Formal Framework for Specifying Sequent Calculus Proof Systems, Theor. Comput. Sci., 474, 2013, 98–116.
• [27] Miller, D., Saurin, A.: From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic, CSL (J. Duparc, T. A. Henzinger, Eds.), 4646, Springer, 2007.
• [28] Nigam, V., Pimentel, E., Reis, G.: Specifying Proof Systems in Linear Logic with Subexponentials, Electr. Notes Theor. Comput. Sci., 269, 2011, 109–123.
• [29] Tiu, A., Momigliano, A.: Cut Elimination for a Logic with Induction and co-Induction, J. Applied Logic, 10(4), 2012, 330–367.
• [30] Troelstra, A. S., Schwichtenberg, H.: Basic Proof Theory (2nd Ed.), vol. 43 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2000.
• [31] Waaler, A., Wallen, L.: Tableaux for Intuitionistic Logics, in: Handbook of Tableaux Methods (M. D’Agostini, D. Gabbay, R. H¨ahnle, Eds.), Kluwer, 1999, 255–296.