×

Efficient loop-check for backward proof search in some non-classical propositional logics. (English) Zbl 1415.03023

Migliolo, P. (ed.) et al., Theorem proving with analytic tableaux and related methods. 5th international workshop, TABLEAUX ’96, Terrasini, Palermo, Italy, May 15–17, 1996. Proceedings. Berlin: Springer-Verlag. Lect. Notes Comput. Sci. 1071, 210-225 (1996).
Summary: We consider the modal logics \(\mathsf{KT}\) and \(\mathsf{S4}\), the tense logic \(\mathsf{K}_{\mathsf{t}}\), and the fragment \(\mathsf{IPC}_{(\wedge,\rightarrow)}\) of intuitionistic logic.
For these logics backward proof search in the standard sequent or tableau calculi does not terminate in general. In terms of the respective Kripke semantics, there are several kinds of non-termination: loops inside a world (\(\mathsf{KT}\)), infinite resp. looping branches (\(\mathsf{S4}\), \(\mathsf{IPC}_{(\wedge,\rightarrow)}\)), and infinite branching degree (\(\mathsf{K}_{\mathsf{t}}\)).
We give uniform sequent-based calculi that contain specifically tailored loop-checks such that the efficiency of proof search is not deteriorated. Moreover all these loop-checks are easy to implement and can be combined with optimizations.
Note that our calculus for \(\mathsf{S4}\) is not a pure contraction-free sequent calculus, but this (theoretical) defect does not hinder its application in practice.
For the entire collection see [Zbl 0939.00023].

MSC:

03B35 Mechanization of proofs and logical operations
03B20 Subsystems of classical logic (including intuitionistic logic)
03B45 Modal logic (including the logic of norms)

Software:

LWB
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Brian F. Chellas. \(Modal logic: an introduction\). Cambridge University Press, 1980. · Zbl 0431.03009
[2] Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. \(The Journal of Symbolic Logic\), 57(3):795-807, 1992. · Zbl 0761.03004
[3] Melvin Fitting. \(Proof Methods for Modal and Intuitionistic Logics\). Reidel, Dordrecht, 1983. · Zbl 0523.03013
[4] Melvin Fitting. Basic modal logic. In Dov M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, \(Handbook of Logic in Artificial Intelligence and Logic Programming\), volume 1, pages 368-448. Clarendon Press, Oxford, 1993.
[5] D M Gabbay. Algorithmic Proof with Diminishing Resources Part 1. In E. Börger, editor, \(CSL 90\), LNCS 533, pages 156-173, 1991. · Zbl 0811.68111
[6] Rajeev Goré. Tableau methods for modal and temporal logics. Technical report, TR-15-95, Automated Reasoning Project, Australian National University, Canberra, Australia, 1995. To appear in Handbook of Tableau Methods, Kluwer, 199?.
[7] Rajeev Goré, Wolfgang Heinle, and Alain Heuerding. Relations between propositional normal modal logics: an overview. Technical report, TR-16-95, Automated Reasoning Project, Australian National University, Canberra, Australia, 1995. · Zbl 0884.03005
[8] Alain Heuerding, Gerhard Jäger, Stefan Schwendimann, and Michael Seyfried. Prepositional logics on the computer. In Peter Baumgartner, Reiner Hähnle, and Joachim Posegga, editors, \(Theorem Proving with Analytic Tableaux and Related Methods\), LNCS 918, pages 310-323, 1995.
[9] Jörg Hudelmaier. An \(O(n\) log \(n\))-space decision procedure for intuitionistic propositional logic. \(Journal of Logic and Computation\), 3(1):63-75, 1993. · Zbl 0788.03010
[10] Jörg Hudelmaier. On a contraction free sequent calculus for the modal logic S4. In \(TABLEAUX 94. 3rd Workshop on Theorem Proving with Analytic Tableaux and Related Methods\), 1994.
[11] S.C. Kleene. \(Introduction to Metamathematics\). North-Holland, Amsterdam, 1952. · Zbl 0047.00703
[12] Richard E. Ladner. The computational complexity of provability in systems of modal prepositional logic. \(SIAM Journal on Computing\), 6(3):467-480, 1977. · Zbl 0373.02025
[13] LWBtheory. http://1wbwww.unibe.ch:8080/LWBtheory.html, 1995.
[14] Nicholas Rescher and Alasdair Urquhart. \(Temporal Logic\). Springer, 1971.
[15] Michael Seyfried. A sequent calculus for proof search in the (→, ∧)-fragment of intuitionistic logic. Unpublished, 1994.
[16] Heinrich Zimmermann. A directed tree calculus for minimal tense logic. Master’s thesis, IAM, University of Berne, Switzerland, 1995.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.