Focused labeled proof systems for modal logic

Dale Miller 1, 2 Marco Volpe 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : 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.
Type de document :
Communication dans un congrès
20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger
Contributeur : Marco Volpe <>
Soumis le : vendredi 9 octobre 2015 - 14:56:46
Dernière modification le : jeudi 10 mai 2018 - 02:06:34
Document(s) archivé(s) le : dimanche 10 janvier 2016 - 10:21:04


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01213858, version 1


Dale Miller, Marco Volpe. Focused labeled proof systems for modal logic. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. 〈hal-01213858〉



Consultations de la notice


Téléchargements de fichiers