Modal theorem proving

1. M. Abadi and Z. Manna, “Nonclausal temporal deduction,” in Logics of Programs (R. Parikh, ed.), Springer-Verlag LNCS 193, 1985, pp. 1–15.

   Google Scholar 

2. M. Abadi and Z. Manna, “A timely resolution,” Proceedings of the Symposium on Logic in Computer Science (LICS), 1986.

   Google Scholar 

3. L. Fariñas del Cerro, “Temporal reasoning and termination of programs,” Eighth International Joint Conference on Artificial Intelligence, 1983, pp. 926–929.

   Google Scholar 

4. L. Fariñas del Cerro, “Un principe de résolution en logique modale,” RAIRO Informatique Théorique, Vol. 18, No. 2, 1984, pp. 161–170.

   Google Scholar 

5. L. Fariñas del Cerro, “Resolution modal logics,” in Logics and Models of Concurrent Systems (K.R. Apt, ed.), Springer-Verlag, Heidelberg, 1985, pp. 27–55.

   Google Scholar 

6. M. Fitting, Proof Methods for Modal and Intuitionistic Logics, D. Reidel Publishing Co., Dordrecht, 1983.

   Google Scholar 

7. M. Fitting, private communication.

   Google Scholar 

8. C. Geissler and K. Konolige, “A resolution method for quantified modal logics of knowledge and belief,” in Theoretical Aspects of Reasoning about Knowledge (J. Halpern, ed.), Morgan Kaufmann Publishers, Palo Alto, 1986, pp. 309–324.

   Google Scholar 

9. G.E. Hughes and M.J. Cresswell, An Introduction to Modal Logic, Methuen & Co., London, 1968.

   Google Scholar 

10. J.Y. Halpern and Y. Moses, “Knowledge and Common Knowledge in a Distributed Environment,” Third ACM Conference on the Principles of Distributed Computing, 1984, pp. 50–61. A revised version appears as IBM RJ 4421, 1984.

    Google Scholar 

11. K. Konolige, A Deduction Model of Belief and its Logics, Ph.D. Thesis, Computer Science Department, Stanford University, 1984.

    Google Scholar 

12. D. McDermott, “Nonmonotonic Logic II: Nonmonotonic Modal Theories,” Journal of the ACM, Vol. 29, No. 1, Jan. 1982, pp. 33–57.

    Article  Google Scholar 

13. N.V. Murray, “Completely nonclausal theorem proving,” Artificial Intelligence, Vol. 18, No. 1, January 1982, pp. 67–85.

    Article  Google Scholar 

14. Z. Manna and R. Waldinger, “A deductive approach to program synthesis,” ACM Transactions on Programming, Languages, and Systems, Vol. 2, No. 1, Jan. 1980, pp. 90–121.

    Google Scholar 

15. Z. Manna and R. Waldinger, “Special relations in automated deduction,” Journal of the ACM, Vol. 33, No. 1, Jan. 1986, pp. 1–59.

    Article  Google Scholar 

16. Z. Manna and R. Waldinger, “Special relations in program-synthetic deduction,” Report No. STAN-CS-82-902, Computer Science Department, Stanford University, March 1982.

    Google Scholar 

17. A. Pnueli, “The temporal logic of programs,” 18th Annual Symposium on Foundations of Computer Science, 1977, pp. 46–57.

    Google Scholar 

18. 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.

    Article  Google Scholar 

19. P. Wolper, “Temporal Logic can be more expressive,” 22nd Annual Symposium on Foundations of Computer Science, 1981, pp. 340–348.

    Google Scholar 

Download references