Abstract
In this paper we present a translation principle, called the axiomatic translation, for reducing propositional modal logics with background theories, including triangular properties such as transitivity, Euclideanness and functionality, to decidable logics. The goal of the axiomatic translation principle is to find simplified theories, which capture the inference problems in the original theory, but in a way that is more amenable to automation and easier to deal with by existing theorem provers. The principle of the axiomatic translation is conceptually very simple and can be largely automated. Soundness is automatic under reasonable assumptions, and termination of ordered resolution is easily achieved, but the non-trivial part of the approach is proving completeness.
We thank Hans de Nivelle and Dmitry Tishkovsky for valuable discussions and suggestions. Support through research grants GR/M36700 and GR/M88761 from the UK Government’s EPSRC is gratefully acknowledged.
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.
References
De Giacomo, G.: Eliminating “converse” from converse PDL. J. Logic, Language and Inform. 5(2), 193–208 (1996)
De Nivelle, H., Schmidt, R.A., Hustadt, U.: Resolution-based methods for modal logics. Logic J. IGPL 8(3), 265–292 (2000)
Demri, S.: The complexity of regularity in grammar logics and related modal logics. Journal of Logic and Computation 11(6), 933–960 (2001)
Demri, S., de Nivelle, H.: Deciding regular grammar logics with converse through first-order logic (2002) (manuscript)
Demri, S., Goré, R.: Tractable transformations from modal provability logics into first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 16–30. Springer, Heidelberg (1999)
Gabbay, D.M.: Decidability results in non-classical logics. Ann. Math. Logic 8, 237–295 (1975)
Ganzinger, H., Meyer, C., de Nivelle, H.: The two-variable guarded fragment with transitive relations. In: Proc. LICS, pp. 24–34. IEEE Computer Society, Los Alamitos (1999)
Hustadt, U., Dixon, C., Schmidt, R.A., Fisher, M.: Normal forms and proofs in combined modal and temporal logics. In: Kirchner, H. (ed.) FroCos 2000. LNCS (LNAI), vol. 1794, pp. 73–87. Springer, Heidelberg (2000)
Hustadt, U., Schmidt, R.A.: On the relation of resolution and tableaux proof systems for description logics. In: Proc. IJCAI 1999, pp. 110–115. Morgan Kaufmann, San Francisco (1999)
Kracht, M.: Tools and Techniques in Modal Logic. Studies in Logic, vol. 142. Elsevier, Amsterdam (1999)
Kracht, M.: Reducing modal consequence relations. J. Logic Computat. 11(6), 879–907 (2001)
Kracht, M.: Notes on the space requirements for checking satisfiability in modal logics. To appear in Advances in Modal Logic 4 (2002)
Lutz, C.: Complexity of terminological reasoning revisited. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS (LNAI), vol. 1705, pp. 181–200. Springer, Heidelberg (1999)
Ohlbach, H.J.: Combining Hilbert style and semantic reasoning in a resolution framework. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS (LNAI), vol. 1421, pp. 205–219. Springer, Heidelberg (1998)
Schmidt, R.A., Hustadt, U.: A principle for incorporating axioms into the firstorder translation of modal formulae. Preprint CSPP-22, Univ. Manchester, UK (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schmidt, R.A., Hustadt, U. (2003). A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive