Abstract
This chapter is about the basic modal logic K and its multimodal version K n . We also present the basic description logic ALC, which can be viewed as a notational variant of K n . The implementation of reasoning methods for all these logics can be done by means of the most basic rules, that are combined by the most basic strategies: fair strategies.
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
Notes
- 1.
We recall that although LoTREC does not display parentheses around <> Q & <>(R v ~P) because & is declared to be associative, we nevertheless did so here—just by declaring & to be non-associative in the language tab—in order to make clear the order of decomposition of A. That order is determined by the way we wrote down A in LoTREC’s prefix notation, viz. as
and nec P and pos Q or pos R not P
as opposed to and and nec P pos Q or pos R not P.
- 2.
We have already mentioned in Sect. 3.4 that the node name w should in principle also be declared to be a variable. However, there are no constant symbols denoting particular nodes in LoTREC. We therefore write w instead of variable w: by convention, the first argument of the ‘add’ action is always a variable.
- 3.
ToDo A verifier que c’est bien different (y avait une erreur trouvee par Teddy).
References
P. Blackburn, J.F.A.K. van Benthem, and F. Wolter. Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning. Elsevier Science, New York, 2006.
P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 2001.
E.W. Beth. Semantic entailment and formal derivability. In Mededlingen van de Koninklijke Nederlandse Akademie van Wetenschappen, Afdeling Letterkunde, N.R, volume 18(3), pages 309–342, 1955. Reprinted in Jaakko Intikka (ed.) The Philosophy of Mathematics, Oxford University Press, 1969.
F. Baader and U. Sattler. Tableau algorithms for description logics. Studia Logica, 69:2001, 2000.
A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford Logic Guides. Oxford University Press, London, 1997.
M. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel, Dordrecht, 1983.
D.M. Gabbay, A. Kurucz, F. Wolter, and M. Zakharyaschev. Many-Dimensional Modal Logics: Theory and Applications, volume 148 of Studies in Logic and the Foundations of Mathematics. Elsevier, Amsterdam, 2003.
R. Goré. Tableau methods for modal and temporal logics. In M. D’Agostino, D.M. Gabbay, R. Hähnle, and J. Posegga, editors, Handbook of Tableau Methods, pages 297–396. Hingham, MA, USA. Kluwer Academic, Dordrecht, 1999.
I. Horrocks. The fact system. In H. de Swart, editor, Proc. of the 2nd Int. Conf. on Analytic Tableaux and Related Methods (TABLEAUX’98), volume 1397 of Lecture Notes in Artificial Intelligence, pages 307–312. Springer, Berlin, 1998.
I. Horrocks. Using an expressive description logic: FaCT or fiction. In Proc. of the 6th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’98), pages 636–647, 1998.
T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle/HOL—A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, Berlin, 2002.
L.C. Paulson. The foundation of a generic theorem prover, Journal of Automated Reasoning, 5, 1989.
R. Smullyan. First Order-Logic. Dover, New York, 1995. First print: 1968.
D. Tsarkov and I. Horrocks. Fact++ description logic reasoner: system description. In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2006), volume 4130 of Lecture Notes in Artificial Intelligence, pages 292–297. Springer, Berlin, 2006.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer Basel AG
About this chapter
Cite this chapter
Gasquet, O., Herzig, A., Said, B., Schwarzentruber, F. (2014). The Basics of the Model Construction Method. In: Kripke’s Worlds. Studies in Universal Logic. Birkhäuser, Basel. https://doi.org/10.1007/978-3-7643-8504-0_3
Download citation
DOI: https://doi.org/10.1007/978-3-7643-8504-0_3
Publisher Name: Birkhäuser, Basel
Print ISBN: 978-3-7643-8503-3
Online ISBN: 978-3-7643-8504-0
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)