Algorithms for Guiding Clausal Temporal Resolution

  • M. Carmen Fernández Gago
  • Michael Fisher
  • Clare Dixon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2479)


Clausal temporal resolution is characterised by a translation of the formulae whose satisfiability is to be established to a normal form, step resolution (similar to classical resolution) on formulae occurring at the same states and temporal resolution between formulae describing properties over a longer period. The most complex part of the method occurs in searching for candidates for the temporal resolution operation, something that may need to be carried out several times.

In this paper we consider a new technique for finding the candidates for the temporal resolution operation. Although related to the previously developed external search procedure, this new approach not only allows the temporal resolution operation to be carried out at any moment, but also simplifies any subsequent search required for similar temporal formulae.

Finally, in contrast with previous approaches, this search can be seen as an inherent part of the resolution process, rather than an external procedure that is only called in certain situations.


Temporal Resolution Temporal Logic Linear Temporal Logic Step Resolution Previous Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    M. Abadi and Z. Manna. Temporal Logic Programming. Journal of Symbolic Computation, 8: 277–295, 1989.zbMATHMathSciNetCrossRefGoogle Scholar
  2. 2.
    M. Abadi and Z. Manna. Nonclausal Deduction in First-Order Temporal Logic. ACM Journal, 37(2):279–317, April 1990.Google Scholar
  3. 3.
    A. Cavalli and L. Farinas del Cerro. A Decision Method for Linear Temporal Logic. In R.E. Shostak, editor, Proceedings of the 7th International Conference on Automated Deduction, volume 170 of Lecture Notes in Computer Science, pages 113–127. Springer-Verlag, 1984.CrossRefGoogle Scholar
  4. 4.
    J. Chomicki and D. Niwinski. On the Feasibility of Checking Temporal Integrity Constraints. Journal of Computer and System Sciences, 51(3):523–535, December 1995.Google Scholar
  5. 5.
    C. Dixon. Temporal Resolution using a Breadth-First Search Algorithm. Annals of Mathematics and Artificial Intelligence, 22:87–115, 1998.zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    C. Dixon and M. Fisher. The Set of Support Strategy in Temporal Resolution. In Proceedings of TIME-98 the Fifth International Workshop on Temporal Representation and Reasoning, Sanibel Island, Florida, May 1998. IEEE Computer Society Press.Google Scholar
  7. 7.
    M.C. Fernández-Gago. Efficient Control of Temporal Reasoning. Transfer Report, Manchester Metropolitan University, 2000.Google Scholar
  8. 8.
    M. Fisher. A Resolution Method for Temporal Logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI), pages 99–104, Sydney, Australia, August 1991. Morgan Kaufman.Google Scholar
  9. 9.
    M. Fisher. A Normal Form for Temporal Logic and its Application in Theorem-Proving and Execution. Journal of Logic and Computation, 7(4):429–456, August 1997.Google Scholar
  10. 10.
    M. Fisher, C. Dixon, and M. Peim. Clausal Temporal Resolution. In Transactions on Computational Logic 2(1), January 2001.Google Scholar
  11. 11.
    D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. The Temporal Analysis of Fairness. In Proceedings of the 7th ACM Symposium on the Principles of Programming Languages, pages 163–173, Las Vegas, Nevada, January 1980.Google Scholar
  12. 12.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992.Google Scholar
  13. 13.
    J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. A CM Journal, 12(1):23–41, January 1965.Google Scholar
  14. 14.
    A. P. Sistla, M. Vardi, and P. Wolper. The Complementation Problem for Buchi Automata with Applications to Temporal Logic. Theoretical Computer Science, 49:217–237, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    G. Venkatesh. A Decision Method for Temporal Logic based on Resolution. Lecture Notes in Computer Science, 206:272–289, 1986.Google Scholar
  16. 16.
    P. Wolper. The Tableau Method for Temporal Logic: An overview. Logique et Analyse, 110-111:119–136, June-Sept 1985.Google Scholar
  17. 17.
    L. Wos, G. Robinson, and D. Carson. Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. ACM Journal, 12:536–541, October 1965.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • M. Carmen Fernández Gago
    • 1
  • Michael Fisher
    • 1
  • Clare Dixon
    • 1
  1. 1.Department of Computer ScienceUniversity of LiverpoolUK

Personalised recommendations