Report Number: CS-TR-86-1100
Institution: Stanford University, Department of Computer Science
Title: Model theorem proving
Author: Abadi, Martin
Author: Manna, Z ohar
Date: May 1986
Abstract: We describe resolution proof systems for several modal
logics. First we present the propositional versions of the
systems and prove their completeness. The first-order
resolution rule for classical logic is then modified to
handle quantifiers directly. This new resolution rule enables
us to extend our propositional systems to complete
first-order systems. The systems for the different modal
logics are closely related.
http://i.stanford.edu/pub/cstr/reports/cs/tr/86/1100/CS-TR-86-1100.pdf