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