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