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 □ (“always”), ◊ (“sometime”), and ○ (“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.
Cite
CITATION STYLE
Abadi, M., & Manna, Z. (1985). Nonclausal temporal deduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 193 LNCS, pp. 1–15). Springer Verlag. https://doi.org/10.1007/3-540-15648-8_1
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
