Abstract
We present a deduction method for propositional modal logics. It is based on a resolution principle for formulas written in a very simple normal form, close to the clausal form for classical logic. It allows us to extend naturally resolution and refinements of resolution to modal logics.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
5 References
Abadi M., Manna Z. Modal theorem proving. 8CAD, LNCS, Springer-Verlag 1986, pp 172–186.
Auffray Y., Enjalbert P., Hebrard J.J., Strategics for modal resolution: results and problems. Rapport du Laboratoire d'Informatique de Caen, 1987.
Balbiani Ph., Fariñas del Cerro L., Herzig A., Declarative semantics for modal logic programs. Rapport LSI, November 1987.
Bieber P., Cooperating with untrusted agents. Rapport LSI, UPS, 1988.
Cialdea M., Une méthode de déduction automatique en logique modale. Thèse Université Paul Sabatier, Toulouse, 1986.
Enjalbert P., Fariñas del Cerro L., Modal resolution in clausal form, Theoretical Computer Sciences, to appear.
Fariñas del Cerro L., A simple deduction method for modal logic. Information Processing Letter 14, 1982.
Fariñas del Cerro L., Herzig A., Quantified modal logic and unification theory. Rapport LSI, UPS, 1988.
Fariñas del Cerro L., Orlowska. E., Automated reasoning in non classical logic. Logique et Analyse, no 110–111, 1985.
Fitting M.C., Proof methods for modal and intuitionistic logics. Methuen & Co., London 1986.
Hughes G.E., Cresswell M.J., A companion to Modal Logic, Methuen & Co. Ltd., London 1986.
Konolige K., Resolution and quantified epistemic logics. 8CAD, LNCS, Springer-Verlag 1986, pp199–209.
Konolige K., A deductive model of belief and its logics. Ph.D. Thesis, Computer Sciences Department, Stanford University 1984.
Mints G., Resolution calculi for modal logics. Proc. of the Academy of Estonian SSR, 1986 (in russian).
Ohlbach H.J., A resolution calculus for modal logics. Report University of Kaiserslautern, 1987.
Wallen L.A., Matrix proof methods for modal logics. In Proc. of 10th ICALP, 1987.
Wrightson, G., Non-classical theorem proving. Journal of automated Reasoning, 1,35–37, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
del Cerro, L.F., Herzig, A. (1988). Linear modal deductions. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012851
Download citation
DOI: https://doi.org/10.1007/BFb0012851
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-19343-2
Online ISBN: 978-3-540-39216-3
eBook Packages: Springer Book Archive