Abstract
The aims of this paper are twofold: First, we review the automated deduction method for normal multi-modal logics which has shown to be the most general and fruitful, namely translation into first-order theories, and more precisely, the functional translation into equational theories with ordered sorts Second, to show how this method can be extended to monotonic modal logics through a translation from the latter into normal modal logics.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Y. Auffray. Résolution modale et logique des chemins. PhD thesis, Université de Caen, France, 1989.
Y. Auffray and P. Enjalbert. Modal theorem proving: An equational viewpoint In Int. Joint Conf. on AI, 1989.
Y Auffray and P. Enjalbert. Modal theorem proving: An equational viewpoint. Journal of Logic and Computation, 1990.
L. Catach. Normal multi-modal logics. In Proc. Nat. Conf. on AI(AAAI'88), pages 491–495, 1988.
L. Catach. Les logiques multi-modales. PhD thesis, Université Paris VI, France, 1989.
B. Chellas. Modal logic: an introduction. Cambridge University Press, 1980.
Ph. Cohen and H. Levesque. Intention=choice+commitment. In Proc. of AAAI, Seattle, 1987.
F. Debart, P. Enjalbert, and M. Lescot. Multi-modal deduction using equational and ordersorted logic. In M. Okada and S. Kaplan, editors, 2nd Conf. on Conditional Rewriting Systems, LNCS. Springer Verlag, 1990.
L. Fariñas del Cerro and A. Herzig. Linear modal deductions. In 9th Int. Conf. on Automated Deduction, volume 310 of LNCS, pages 500–516. Springer Verlag, 1988.
L. Fariñas del Cerro and A. Herzig. Machine Learning, Meta Reasoning and Logics, chapter Deterministic Modal Logics for Automated Deduction. Kluwer Academic Publishers, 1989.
L. Fariñas del Cerro and A. Herzig. Deterministic modal logic for automated deduction. In 9th European Conference on Artificial Intelligence, 1990.
L. Fariñas del Cerro and A. Herzig. Handbook of Logic in Artificial Intelligence, chapter Automated Deduction for Epistemic and Temporal Logics. Oxford University Press, 1995.
O. Gasquet. A unification algorithm for multimodal logics with persistence axiom. In 5th International Workshop on Unification (UNIF'91), Barbizon, France, 1991.
O. Gasquet. Applied Logic: How, What and Why, chapter imization of Deduction for Multi-Modal Logics. Kluwer Academic Publishers, 1995.
J. Halpern. Reasoning about knowledge: an overview. In J. Halpern, editor, Conf. on Theoretical Aspects of Reasoning about Knowledge, pages 1–17. Morgan Kauffmann, 1986.
J. Halpern and Y. Moses. A guide to the modal logic of knowledge and belief. In Proc. of IJCAI, 1985.
D. Harel. Handbook of Philosophical Logic III, chapter Dynamic Logic”. Reidel Publishing Company, 1986.
A. Herzig. Déduction automatique en logique modale et algorithmes d'unification. PhD thesis, Université Paul Sabatier, Toulouse, France, 1989.
G. Hughes and M. J. Cresswell. An Introduction to Modal Logic. Methuen & Co. Ltd, 1968.
G. Hughes and M. J. Cresswell. A Companion to Modal Logic. Methuen & Co. Ltd, 1984.
A. J. I. Jones and I. Pörn. Ideality, sub-ideality and deontic logic. Synthese, 65, 1985.
A. J. I. Jones and I. Pörn. ‘ought and must'. Synthese, 66, 1986.
S. Kraus and D. Lehmann. Automata, Languages and Programing, volume 226 of Lecture Notes in Computer Science, chapter Knowledge, belief and time, pages 186–195. Springer-Verlag, 1986.
H. J. Ohlbach. A resolution calculus for modal logics. In 9th Int. Conf. on Automated Deduction, volume 310 of LNCS. Springer-Verlag, 1988.
H. J. Ohlbach. Semantics-based translation method for modal logics. Journal of Logic and Computation, 1(5):691–746, 1991.
H. J. Ohlbach. imized translation of multi modal logic into predicate logic. In Proc. of International Conference on Logic Programming and Automated Reasoning (LPAR'93), LNAI. Springer-Verlag, 1993.
H. J. Ohlbach and A. Herzig. Parameter structures for parametrized modal operators. In Proc. of Int. Joint Conf. on Artificial Intelligence; 1991.
H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logics. In S. Kanger, editor, Proc. 3rd Scandinavian Logic Symposium 1973, volume 82 of Studies in logic. North-Holland, 1975.
M. Schmidt-Schauß. Computational Aspects of an Order-Sorted Logic with Term Declarations. LNAI. Springer-Verlag, 1989.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gasquet, O., Herzig, A. (1995). Translation-based deduction methods for modal logics. In: Bouchon-Meunier, B., Yager, R.R., Zadeh, L.A. (eds) Advances in Intelligent Computing — IPMU '94. IPMU 1994. Lecture Notes in Computer Science, vol 945. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0035973
Download citation
DOI: https://doi.org/10.1007/BFb0035973
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60116-6
Online ISBN: 978-3-540-49443-0
eBook Packages: Springer Book Archive