BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-85-1056
       ENTRY:: May 01, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Nonclausal temporal deduction
        TYPE:: Technical Report
      AUTHOR:: Abadi, Martin
      AUTHOR:: Manna, Zohar
        DATE:: June 1985
       PAGES:: 20
    ABSTRACT:: We present a proof system for propositional temporal logic.
               This system is based on nonclausal resolution; proofs are
               natural and generally short. Its extension to first-order
               temporal logic is considered.

               Two variants of the system are described. The first one is
               for a logic with $\Box$ ("always"), $\Diamond$ ("sometime"),
               and $\bigcirc$ ("next"). The second variant is an extension
               of the first one to a logic with the additional operators U
               ("until") and P ("precedes"). Each of these variants is
               proved complete.
       NOTES:: [Adminitrivia V1/Prg/19950501]
         END:: STAN//CS-TR-85-1056