Nonclausal deduction in first-order temporal logic

ABSTRACT

This paper presents a proof system for first-order temporal logic. The system extends the nonclausal resolution method for ordinary first-order logic with equality, to handle quantifiers and temporal operators. Soundness and completeness issues are considered. The use of the system for verifying concurrent programs is discussed and variants of the system for other modal logics are also described.

REFERENCES

• 1: M. Abadi, Temporal-logic theorem proving, Stanford University, Stanford, CA, 1987
• 2: Martín Abadi, The power of temporal proofs, Theoretical Computer Science, v.65 n.1, p.35-83, 15 June 1989 [doi>10.1016/0304-3975(89)90138-2]
• 3: Martín Abadi , Zohar Manna, Nonclausal Temporal Deduction, Proceedings of the Conference on Logic of Programs, p.1-15, June 17-19, 1985
• 4: ABADI, M., AND MANNA, Z. A timely resolution. In Proceedings of the 1st Annual Symposium on Logic in Computer Science. IEEE Computer Society, Washington, D.C., 1986, pp. 176-186.
• 5: M Abadi , Z Manna, Modal theorem proving, Proc. of the 8th international conference on Automated deduction, p.172-189, August 1986, Oxford, United Kingdom
• 6: M. Abadi , Z. Manna, Temporal logic programming, Journal of Symbolic Computation, v.8 n.3, p.277-295, Sep. 1989 [doi>10.1016/S0747-7171(89)80070-7]
• 7: Ross Casley, A proof editor for propositional temporal logic, Stanford University, Stanford, CA, 1986
• 8: Ana R. Cavalli, A method of automatic proof for the specification and verification of protocols, Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium, p.100-106, June 06-08, 1984, Montréal, Quebec, Canada, United States
• 9: Ana R. Cavalli , Luis Fariñas del Cerro, A Decision Method for Linear Temporal Logic, Proceedings of the 7th International Conference on Automated Deduction, p.113-127, May 14-16, 1984
• 10: EMERSON, E. A., AND CLARK, E. M. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Prog. 2 (1982), 241-266.
• 11: FITTING, M. Proof Methods for Modal and Intuitionistic Logics. Reidel, Dordrecht, West Germany, 1983.
• 12: FLOYD, R.W. Assigning meanings to programs. In Mathematical Aspects of Computer Science, Proceedings of the 19th Symposium in Applied Mathematics. American Mathematical Society, Providence, R.I., 1967, pp. 19-32.
• 13: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 14: GEORGEFF, M. Communication and interaction in multi-agent planning. In Proceedings of the American Association for Artificial Intelligence. AAAI, Menlo Park, Calif., 1983, pp. 125-129.
• 15: Joseph Y. Halpern , Yoram Moses, Knowledge and common knowledge in a distributed environment, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.50-61, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806735]
• 16: HALPERN, B., AND OWICKI, S. Modular verification of computer communication protocols. IEEE Trans. Commun. COM-31, 1 (Jan. 1983), 56-68.
• 17: HAREL, D. Dynamic logic. In Handbook of Philosophical Logic, vol. II. D. Gabbay and F. Guenthner, eds. Reidel, Dordrecht, West Germany, 1984, pp. 497-604.
• 18: HUGHES, G. E., AND CRESSWELL, M.J. An Introduction to Modal Logic. Methuen & Co., London, England, 1968.
• 19: Leslie Lamport, Specifying Concurrent Program Modules, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.2, p.190-222, April 1983 [doi>10.1145/69624.357207]
• 20: Z Manna , Amir Pnueli, Verification of concurrent programs: a temporal proof system, Stanford University, Stanford, CA, 1983
• 21: Zohar Manna , Amir Pnueli, Adequate proof principles for invariance and liveness properties of concurrent programs, Science of Computer Programming, v.4 n.3, p.257-289, Dec. 1984 [doi>10.1016/0167-6423(84)90003-0]
• 22: Zohar Manna , Richard Waldinger, A Deductive Approach to Program Synthesis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.90-121, Jan. 1980 [doi>10.1145/357084.357090]
• 23: MANNA, Z., AND WALDINGER, R. Special relations in program-synthetic deduction. Rep. No. STAN-CS-82-902. Comput. Sci. Dept., Stanford Univ., Stanford, Calif., Mar., 1982.
• 24: Zohar Manna , Richard Waldinger, The logical basis for computer programming. Volume 1: deductive reasoning, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1985
• 25: Zohar Manna , Richard Waldinger, Special relations in automated deduction, Journal of the ACM (JACM), v.33 n.1, p.1-59, Jan. 1986 [doi>10.1145/4904.4905]
• 26: Zohar Manna , Richard Waldinger, The logical basis for computer programming: vol. 2, deductive systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 27: Zohar Manna , Pierre Wolper, Synthesis of Communicating Processes from Temporal Logic Specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.6 n.1, p.68-93, Jan. 1984 [doi>10.1145/357233.357237]
• 28: Drew McDermott, Nonmonotonic Logic II: Nonmonotonic Modal Theories, Journal of the ACM (JACM), v.29 n.1, p.33-57, Jan. 1982 [doi>10.1145/322290.322293]
• 29: Benjamin Charles Moszkowski, Reasoning about digital circuits, 1983
• 30: MURRAY, N.V. Completely nonclausal theorem proving. Artif Intell. 18, I (Jan. 1982), 67-85.
• 31: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 32: PARIKH, R. A decidability result for second order process logic. In Proceedings of the 19th Annual IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1978, pp. 177-183.
• 33: David A Plaisted, A decision procedure for combinations of propositional temporal logic and other specialized theories, Journal of Automated Reasoning, v.2 n.2, p.171-190, 1986 [doi>10.1007/BF02432150]
• 34: PNUELI, A. The temporal semantics of concurrent programs. Theoret. Comput. Sci. 13 (1981), 45-60.
• 35: J. A. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM (JACM), v.12 n.1, p.23-41, Jan. 1965 [doi>10.1145/321250.321253]
• 36: A. P. Sistla , E. M. Clarke, The complexity of propositional linear temporal logics, Journal of the ACM (JACM), v.32 n.3, p.733-749, July 1985 [doi>10.1145/3828.3837]
• 37: SMULLYAN, R.M. First-Order Logic. Springer-Verlag, Berlin, 1968.
• 38: G. Venkatesh, A Decision Method for Temporal Logic Based on Resolution, Proceedings of the Fifth Conference on Foundations of Software Technology and Theoretical Computer Science, p.272-289, December 16-18, 1985
• 39: WOLPER, P. Temporal logic can be more expressive, lnfi Control 56, 1-2 (1983), 72-99.
• 40: WOLPER, P. The tableau method for temporal logic: An overview. Logique et Analyse 1 I0-111, (1985), 119-136.
• 41: WOLPER, P., VARDI, M. Y., AND SISTLA, A.P. Reasoning about infinite computation paths. In Proceedings of the 24th Annual IEEE Symposium on Foundations of Computer Science. IEEE, New York, 1983, pp. 185-194.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

General Terms:
Theory, Verification