Skip to main content
SpringerLink
Log in

Identity in modal logic theorem proving

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

THINKER is an automated natural deduction first-order theorem proving program. This paper reports on how it was adapted so as to prove theorems in modal logic. The method employed is an “indirect semantic method”, obtained by considering the semantic conditions involved in being a valid argument in these modal logics. The method is extended from propositional modal logic to predicate modal logic, and issues concerning the domain of quantification and “existence in a world's domain” are discussed. Finally, we look at the very interesting issues involved with adding identity to the theorem prover in the realm of modal predicate logic. Various alternatives are discussed.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. B. Chellas,Modal Logic, Cambridge University Press, 1980.

  2. P. Jackson endH. Reichgelt,A general proof method for first order modal logic,IJCAI-10, 1987, pp. 942 – 944.

  3. D. Kalish andR. Montague,Logic Hartcourt, Brace, Janovich, 1964.

    Google Scholar 

  4. D. Kalish, R. Montague andG. Mar,Logic, Hartcourt, Brace, Janovich, 1980.

    Google Scholar 

  5. S. Kripke,Identity and necessity, in M. Munitz, ed.,Identity and Individuation, New York University Press, 1971, pp. 135 – 164.

  6. S. Kripke,Naming and necessity, in D. Davidson and G. Harman, eds,Semantics of Natural Language, D. Reidel Publ. Co., Dordrecht 1972, pp. 253–355 and 763 – 769.

    Google Scholar 

  7. M. McRobbie, R. Meyer andP. Thistlewaite,Towards efficient ‘knowledge-based’ automated theorem proving for non-standard logics,CADE-9, Springer-Verlag 1988, pp. 197 – 217.

  8. C. Morgan,Methods for automated theorem proving in non-classical logics,IEEE Trans. on Computers, 1976, pp. 852 – 862.

  9. C. Morgan,Autologic,Logique et Analyse, 1985, pp. 257 – 282.

  10. H. Ohlbach,A resolution calculus for modal logics,CADE-9, Springer-Verlag 1988, pp. 500 – 516.

  11. F. J. Pelletier,Completely Non-Causal, Completely Heuristic-Driven, Automatic theorem Proving Tech. Report TR82-7, Dept. Computing Science, Univ. Alberta, 1982.

    Google Scholar 

  12. F. J. Pelletier,Further Developments in THINKER, an Automated Theorem Prover Tech. Report TR-ARP-16/87 Automated Reasoning Project, Australia National University, 1987.

    Google Scholar 

  13. F. J. Pelletier,The philosophy of automated theorem proving,Proceedings of IJCAI-91, 1991.

  14. R. Smullyan,First Order Logic, Springer-Verlag 1968.

  15. P. Thistlewaite, M. McRobbie andR. Meyer,Automated Theorem Proving in Non-Classical Logics, Pitman, 1987.

  16. P. Thistlewaite, R. Meyer andM. McRobbie,Advanced theorem proving techniques for relevant logics,Logique et Analyse, 1985, pp. 233 – 258.

  17. A. Whitehead andB. Russell,Principia Mathematica, Cambridge University Press 1910.

  18. G. Wrightson,Non-classical logic theorem proving,Journal of Automated Reasoning, 1985, pp. 35 – 37.

Download references

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Alberta, 615 General Services Building, T6G 2H1, Edmonton, Alberta, Canada

    Francis J. Pelletier

Authors
  1. Francis J. Pelletier
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

About this article

Cite this article

Pelletier, F.J. Identity in modal logic theorem proving. Stud Logica 52, 291–308 (1993). https://doi.org/10.1007/BF01058393

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01058393

Keywords

Search

Navigation