BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-86-1100
       ENTRY:: May 01, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Model theorem proving
        TYPE:: Technical Report
      AUTHOR:: Abadi, Martin
      AUTHOR:: Manna, Zohar
        DATE:: May 1986
       PAGES:: 22
    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.
       NOTES:: [Adminitrivia V1/Prg/19950501]
         END:: STAN//CS-TR-86-1100