BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-86-1106
       ENTRY:: May 01, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: A timely resolution
        TYPE:: Technical Report
      AUTHOR:: Abadi, Martin
      AUTHOR:: Manna, Zohar
        DATE:: April 1986
       PAGES:: 24
    ABSTRACT:: We present a novel proof system R for First-order (Linear)
               Temporal Logic. This system extends our Propositional
               Temporal Logic proof system ([AM]). The system R is based on
               nonclausal resolution; proofs are natural and generally
               short. Special quantifier rules, unification techniques, and
               a resolution rule are introduced. We relate R to other proof
               systems for First-order Temporal Logic and discuss
               completeness issues. The system R should be useful as a tool
               for such tasks as verification of concurrent programs and
               reasoning about hardware devices.
       NOTES:: [Adminitrivia V1/Prg/19950501]
         END:: STAN//CS-TR-86-1106