Focused labeled proof systems for modal logic

Conference object English OPEN
Miller , Dale ; Volpe , Marco (2015)
  • Publisher: HAL CCSD
  • Subject: [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | Geometric formulas | Labeled proof systems | Focused proof systems | Modal logic
    acm: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
    arxiv: Computer Science::Logic in Computer Science

International audience; Focused proofs are sequent calculus proofs that group inference rules into alternating positive and negative phases. These phases can then be used to define macro-level inference rules from Gentzen's original and tiny introduction and structural rules. We show here that the inference rules of labeled proof systems for modal logics can similarly be described as pairs of such phases within the LKF focused proof system for first-order classical logic. We consider the system G3K of Negri for the modal logic K and define a translation from labeled modal formulas into first-order polarized formulas and show a strict correspondence between derivations in the two systems, i.e., each rule application in G3K corresponds to a bipole—a pair of a positive and a negative phases—in LKF. Since geometric axioms (when properly polarized) induce bipoles, this strong correspondence holds for all modal logics whose Kripke frames are characterized by geometric properties. We extend these results to present a focused labeled proof system for this same class of modal logics and show its soundness and completeness. The resulting proof system allows one to define a rich set of normal forms of modal logic proofs.
  • References (19)
    19 references, page 1 of 2

    1. Jean-Marc Andreoli. Logic programming with focusing proofs in linear logic. J. of Logic and Computation, 2(3):297{347, 1992.

    2. Patrick Blackburn and Johan Van Benthem. Modal logic: a Semantic Perspective. In Handbook of Modal Logic, pp 1{82. Elsevier, 2007.

    3. Zakaria Chihani, Dale Miller, and Fabien Renaud. Foundational proof certi cates in rst-order logic. In CADE 24, LNAI 7898, pp. 162{177, 2013.

    4. Zakaria Chihani, Tomer Libal, and Giselle Reis. System Description: The Proof Certi er Checkers. To appear in Tableaux 2015.

    5. Roy Dyckho and Sara Negri. Proof analysis in intermediate logics. Archive for Mathematical Logic, 51(1-2):71{92, 2012.

    6. Roy Dyckho and Sara Negri. Geometrisation of rst-order logic. The Bulletin of Symbolic Logic, 21:123{163, 6 2015.

    7. Melvin Fitting. Modal proof theory. In Frank Wolter Patrick Blackburn, Johan van Benthem, editor, Handbook of Modal Logic, pages 85{138. Elsevier, 2007.

    8. Dov M. Gabbay. Labelled Deductive Systems. Clarendon Press, 1996.

    9. Jean-Yves Girard. On the meaning of logical rules I: syntax vs. semantics. In Berger and Schwichtenberg, eds, Computational Logic, pp. 215{272. Springer, 1999.

    10. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theor. Comput. Sci., 410(46):4747{4768, 2009.

  • Metrics
    No metrics available
Share - Bookmark