Abstract
In this paper we present a deduction method for quantified modal logics via extensions of the classical unification algorithm. We show that deductions in modal logics can be formulated as particular problems in unification theory.
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
Abadi M., Manna Z., Modal Theorem Proving. 8CAD, Lecture Notes on Computer Science, Springer-Verlag 1986, pp. 172–186.
Auffray, Y., Enjalbert, P., Demonstration de Théorèmes en Logique Modale — Un Point de Vue Equationnel. JELIA 88, Roscoff, 1988.
Cialdea M., Une Methode de Deduction Automatique en Logique Modale. These Université Paul Sabatier, Toulouse, 1986.
Colmerauer A., Equations and Inequations on Finite and Infinite Trees. FGCS’84 Proceedings 1984, pp. 85–89.
Fariñas del Cerro L., Un Principe de Resolution en Logique Modale. RAIRO 1983,18,2, pp. 161–170.
Fariñas del Cerro L., Herzig A., Quantified Modal Logic and Unification Theory. Report Université Paul Sabatier, Apr. 1989 (2nd draft).
Fitting M., First Order Modal Tableaux. Journal of Automated Reasoning, Vol. 4, No. 2, June 1988, pp.191–214.
Herzig A., Raisonement Automatique en Logique Modale et Algorithmes d’Unification. Thèse Université Paul Sabatier, Toulouse, 1989.
Hughes G. E., Cresswell, M. J., A Companion to Modal Logic. Methuen & Co. Ltd., London 1986.
Jackson P., Reichgelt H., A General Proof Method for First-Order Modal Logic. International Joint Conference on Artificial Intelligence 1987.
Kirchner C, A New Equational Unification Method: A Generalisation of Martelli-Montanari’s Algorithm. CADE7, Springer-Verlag 1984.
Konolige K., Resolution and Quantified Epistemic Logics. 8CAD, Lecture Notes on Computer Science, Springer Verlag 1986, pp. 199–209.
Lassez L., Maher M. J., Marriott K., Unification Revisited, in: Foundations of Deductive Databases and Logic Programming, J. Minker (ed.), Morgan Kaufmann, Los Altos, 1988.
Ohlbach, H. J., A Resolution Calculus for Modal Logics. CADE9, Lecture Notes on Computer Science, Springer Verlag 1988.
Pécuchet J. P., Equations avec Constantes et Algorithme de Makanin. Thèse Université de Rouen, 1981.
Robinson A., A Machine Oriented Logic Based on the Resolution Principle. Journal of Association of Computing Machinery 12,1965.
Siekmann J., Universal Unification. CAD7, Lecture Notes on Computer Science, Springer Verlag 1984.
Wallen L. A., Matrix Proof Methods for Modal Logic. International Joint Conference on Artifical Intelligence 87, Milan.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Kluwer Academic Publishers
About this chapter
Cite this chapter
del Cerro, L.F., Herzig, A. (1990). Automated Quantified Modal Logic. In: Brazdil, P.B., Konolige, K. (eds) Machine Learning, Meta-Reasoning and Logics. The Kluwer International Series in Engineering and Computer Science, vol 82. Springer, Boston, MA. https://doi.org/10.1007/978-1-4613-1641-1_14
Download citation
DOI: https://doi.org/10.1007/978-1-4613-1641-1_14
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4612-8906-7
Online ISBN: 978-1-4613-1641-1
eBook Packages: Springer Book Archive