Report Number: CS-TR-85-1056
Institution: Stanford University, Department of Computer Science
Title: Nonclausal temporal deduction
Author: Abadi, Martin
Author: Manna, Z ohar
Date: June 1985
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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/85/1056/CS-TR-85-1056.pdf