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.
This research was supported in part by the National Science Foundation under grant MCS-81-11586, by Defense Advanced Research Projects Agency under Contract N00039-84-C-0211, and by the United States Air Force Office of Scientific Research under Contract AFOSR-81-0014.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Cavalli, A., “A method of automatic proof for the specification and verification of protocols,” ACM SIGCOMM 84 Symposium, Montreal, Canada, 1984.
Cavalli, A., and L. Fariñas del Cerro, “A decision method for linear temporal logic,” Seventh Conference on Automated Deduction, Napa, CA, May 1984, pp. 113–127.
Gabbay, D., A. Pnueli, S. Shelah and J. Stavi, “The temporal analysis of fairness,” Seventh ACM Symposium on Principles of Programming Languages, Las Vegas, NV, January 1980, pp. 163–173.
Huet, G. P., “Constrained resolution: a complete method for higher order logic,” Ph.D. Thesis, Case Western University, Jennings Computing Center Report 1117, August 1972.
Huet, G. P., “A unification algorithm for typed λ-calculus,” Theoretical Computer Science, Vol. 1, No. 1, pp. 27–57.
Manna, Z. and A. Pnueli, “Verification of concurrent programs: The temporal framework,” in The Correctness Problem in Computer Science (R.S. Boyer and J S. Moore, eds.), International Lecture Series in Computer Science, Academic Press, London, 1982, pp. 215–273.
Manna, Z. and R. Waldinger, “A deductive approach to program synthesis,” ACM Transactions on Programming Languages and Systems, Vol. 2, No. 1, January 1980, pp. 92–121.
Murray, N. V., “Completely nonclausal theorem proving,” Artificial Intelligence, Vol. 18, No. 1, pp. 67–85, January 1982.
J. A. Robinson, “A machine-oriented logic based on the resolution principle,” Journal of the ACM, Vol. 12, No. 1, January 1965, pp. 23–41.
Wolper, P., “Temporal logic can be more expressive,” Proc. 22nd IEEE Symp. on Foundations of Computer Science, Nashville, 1981, pp. 340–348.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Abadi, M., Manna, Z. (1985). Nonclausal temporal deduction. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_1
Download citation
DOI: https://doi.org/10.1007/3-540-15648-8_1
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15648-2
Online ISBN: 978-3-540-39527-0
eBook Packages: Springer Book Archive