Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1986: 8th International Conference on Automated Deduction pp 199–208Cite as

Resolution and quantified epistemic logics

  • Nondassical Deducation
  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 230))

Abstract

Quantified modal logics have emerged as useful tools in computer science for reasoning about knowledge and belief of agents and systems. An important class of these logics have a possible-world semantics from Kripke. Surprisingly, there has been relatively little work on proof theoretic methods that could be used in automatic deduction systems, although decision procedures for the propositional case have been explored. In this paper we report some general results in this area, including completeness, a Herbrand theorem analog, and resolution methods. Although they are developed for epistemic logics, we speculate that these methods may prove useful in quantified temporal logic also.

This research was made possible in part by a gift from the System Development Foundation, and was also supported by Contract N000140-85-C-0251 from the Office of Naval Research.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M. and Manna, Z. (1985). Nonclausal temporal deduction. Report No. STAN-CS-85-1056, Computer Science Department, Stanford University, Stanford, California.

    Google Scholar 

  2. Fagin, R. and Halpern, J. Y. (1985). Belief, awareness, and limited of the Ninth INternational Joint Conference on AI, Los Angeles, California, pp. 491–501.

    Google Scholar 

  3. Fariñas-del-Cerro, L. (1983). Temporal reasoning and termination of programs. In Proceedings of the Eighth International Joint Conference on Artificial Intelligence, Karlsruhe, West Germany, pp. 926–929.

    Google Scholar 

  4. Geissler, C. and Konolige, K. (1986). A resolution method for quantified modal logics of knowledge and belief. In Proceedings of the Conference on Theoretical Aspects of Reasoning about Knowledge, Monterey, California.

    Google Scholar 

  5. Halpern, J. Y. and Moses, Y. (1984). Knowledge and common knowledge in a distributed environment. In Proceedings of the 3rd ACM Conference on Principles of Distributed Computing, pp. 50–61.

    Google Scholar 

  6. Halpern, J. Y. and Moses, Y. (1985). A guide to the modal logics of knowledge and belief: preliminary draft. In Proceedings of the Ninth International Joint Conference on AI, Los Angeles, California, pp. 479–490.

    Google Scholar 

  7. Hintikka, J. (1962). Knowledge and Belief. Cornell University Press, Ithaca, New York.

    Google Scholar 

  8. Hintikka, J. (1969). Semantics for propositional attitudes. In L. Linsky (ed.), Reference and Modality, Oxford University Press, London (1971), pp. 145–167.

    Google Scholar 

  9. Konolige, K. (1984). A Deduction Model of Belief and its Logics. Doctoral thesis, Stanford University Computer Science Department Stanford, California.

    Google Scholar 

  10. Kripke, S. A. (1959). A Completeness Theorem in Modal Logic. Journal of Symbolic Logic 24, pp. 1–14.

    Google Scholar 

  11. Levesque, H. J. (1982). A Formal Treatment of Incomplete Knowledge Bases. FLAIR Technical Report No. 614, Fairchild Laboratories, Palo Alto, California.

    Google Scholar 

  12. Levesque, H. J. (1984). A logic of implicit and explicit belief. In Proceedings of the National Conference on Artificial Intelligence, Houston, Texas, pp. 198–202.

    Google Scholar 

  13. McCarthy, J. et al. (1978). On the Model Theory of Knowledge. Memo AIM-312, Stanford University, Stanford.

    Google Scholar 

  14. Moore, R. C. (1980). Reasoning About Knowledge and Action. Artificial Intelligence Center Technical Note 191, SRI International, Menlo Park, California.

    Google Scholar 

  15. Robinson, J. A. (1965). A machine-oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, pp. 23–41.

    Google Scholar 

  16. Sato, M. (1976). A study of Kripke-type models for some modal logics by Gentzen's sequential method. Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan.

    Google Scholar 

  17. Smullyan, R. M. (1971). First-order logic. Springer-Verlag, New York.

    Google Scholar 

  18. Stickel, M. E. (1985). Automated deduction by theory resolution. Proceedings of the Ninth International Joint Conference on Artificial Intelligence, Los Angeles, California.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Artificial Intelligence Center and CSLI SRI International, 94025, Menlo Park, California, USA

    Kurt Konolige

Authors
  1. Kurt Konolige
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jörg H. Siekmann

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Konolige, K. (1986). Resolution and quantified epistemic logics. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_91

Download citation

  • DOI: https://doi.org/10.1007/3-540-16780-3_91

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16780-8

  • Online ISBN: 978-3-540-39861-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation