Identity in modal logic theorem proving

Studia Logica 52 (2):291 - 308 (1993)
  Copy   BIBTEX

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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Analytics

Added to PP
2009-01-28

Downloads
75 (#200,005)

6 months
4 (#315,466)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Logic.Donald Kalish - 1964 - New York,: Harcourt, Brace & World. Edited by Richard Montague.

Add more references