Algorithms for Guiding Clausal Temporal Resolution
- 435 Downloads
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.
KeywordsTemporal Resolution Temporal Logic Linear Temporal Logic Step Resolution Previous Search
Unable to display preview. Download preview PDF.
- 2.M. Abadi and Z. Manna. Nonclausal Deduction in First-Order Temporal Logic. ACM Journal, 37(2):279–317, April 1990.Google Scholar
- 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
- 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.M.C. Fernández-Gago. Efficient Control of Temporal Reasoning. Transfer Report, Manchester Metropolitan University, 2000.Google Scholar
- 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.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.M. Fisher, C. Dixon, and M. Peim. Clausal Temporal Resolution. In Transactions on Computational Logic 2(1), January 2001.Google Scholar
- 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.Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992.Google Scholar
- 13.J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. A CM Journal, 12(1):23–41, January 1965.Google Scholar
- 15.G. Venkatesh. A Decision Method for Temporal Logic based on Resolution. Lecture Notes in Computer Science, 206:272–289, 1986.Google Scholar
- 16.P. Wolper. The Tableau Method for Temporal Logic: An overview. Logique et Analyse, 110-111:119–136, June-Sept 1985.Google Scholar
- 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