Abstract
The main contribution of this work is twofold. It presents a modular tableau calculus, in the free-variable style, treating the main domain variants of quantified modal logic and dealing with languages where rigid and non-rigid designation can coexist. The calculus uses, to this end, light and simple semantical annotations. Such a general proof-system results from the fusion into a unified framework of two calculi previously defined by the second and third authors. Moreover, the work presents a theorem prover, called GQML-Prover, based on such a calculus, which is accessible in the Internet. The fair deterministic proof-search strategy used by the prover is described and illustrated via a meaningful example.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
B. Beckert and R. Goré. Free variable tableaux for propositional modal logics. In Proc. of TABLEAUX’97, pages 91–106. Springer, 1997.
S. Cerrito and M. Cialdea Mayer. Free-variable tableaux for constant-domain quantified modal logic with rigid and non-rigid designation. In First Int. Joint Conf. on Automated Reasoning (IJCAR 2001), pages 137–151. Springer, 2001.
M. Cialdea Mayer and S. Cerrito. Variants of first-order modal logics. In Proc. of TABLEAUX 2000, pages 175–189. Springer, 2000.
M. Cialdea Mayer and S. Cerrito. Ground and free-variable tableaux for variants of quantified modal logics. Studia Logica, 69:97–131, 2001.
F. M. Donini and F. Massacci. EXPTIME tableaux for ALC. Artificial Intelligence, 124:87–138, 2000.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. Reidel, 1983.
M. Fitting. First-Order Logic and Automated Theorem Proving. Springer, 1996.
M. Fitting and R Mendelsohn. First-Order Modal Logic. Kluwer, 1998.
R. Goré. Automated reasoning project. Technical report, TR-ARP-15-95, 1997.
R. Hähnle and P. H. Schmitt. The liberalized δ-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13:211–222, 1994.
U. Hustadt and R. A. Schmidt. Simplification and backjumping in modal tableau. In Proc. of TABLEAUX’98, pages 187–201. Springer, 1998.
Jens Otten. ileanTAP: An intuitionistic theorem prover. In Proc. of TABLEAUX’97, pages 307–312. Springer, 1997.
J. Posegga and P. Schmitt. Implementing semantic tableaux. In M. D’Agostino, G. Gabbay, R. Hähnle, and J. Posegga, editors, Handbook of tableau method, pages 581–629. Kluwer, 1999.
V. Thion. A strategy for free variable tableaux for variant of quantified modal logics. Technical report, L.R.I., 2002. http://www.lri.fr/~thion.
L. A. Wallen. Automated Deduction in Nonclassical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics. MIT Press, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Thion, V., Cerrito, S., Mayer, M.C. (2002). A General Theorem Prover for Quantified Modal Logics. In: Egly, U., Fermüller, C.G. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2002. Lecture Notes in Computer Science(), vol 2381. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45616-3_19
Download citation
DOI: https://doi.org/10.1007/3-540-45616-3_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43929-5
Online ISBN: 978-3-540-45616-2
eBook Packages: Springer Book Archive