Abstract
This paper describes how to use Otter, a resolution based theorem prover for classical propositional and first-order logics to implement Fisher’s temporal resolution method. Fisher’s clausal temporal resolution method involves both classical-style ‘step’ resolution within states and ‘temporal’ resolution over states. As the translation to a normal form removes most of the temporal operators, and the resolution within states is very similar to resolution in classical logics, most of the inferences required for the step resolution phase can be performed by Otter after a simple translation into classical propositional logic. However, the application of the temporal resolution rule is more complex, requiring a search for sets of formulae that together imply an invariant property, for resolution with an eventuality formula. We suggest how Otter can be used to fulfil the obligations of a particular algorithm that performs this search. The correctness of the method is discussed and we conclude by outlining how it has helped develop a prototype theorem prover based on Fisher’s method.
This work was supported partially by an EPSRC PhD Studentship and partially by EPSRC Research Grant GR/K57282
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Y. Auffray and P. Enjalbert. Modal Theorem Proving: An Equational Viewpoint. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI), pages 441-445, Detroit, USA, 1989. Morgan Kaufmann.
H. Barringer. Using Temporal Logic in the Compositional Specification of Concurrent Systems. In A. P. Galton, editor, Temporal Logics and their Applications, chapter 2, pages 53–90. Academic Press Inc. Limited, London, December 1987.
M.-C. Chan. The Recursive Resolution Method for Modal Logic. New Generation Computing, 5: 155–183, 1987.
M. Carlsson and J. Widen. SICStus Prolog User’s Manual. Swedish Institute of Computer Science, Kista, Sweden, September 1991.
C. Dixon. Strategies for Temporal Resolution. PhD thesis, Department of Computer Science, University of Manchester, 1995.
C. Dixon. Search Strategies for Resolution in Temporal Logics. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE),volume 1104 of Lecture Notes in Artificial Intelligence,pages 672-687, New Brunswick, New Jersey, July/August 1996. Springer-Verlag.
C. Dixon. Temporal Resolution: Removing Irrelevant Information. In Proceedings of TIME-97 the Fourth International Workshop on Temporal Representation and Reasoning, Daytona Beach, Florida, May 1997.
M. Fisher. A Resolution Method for Temporal Logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence (IJCAI),Sydney, Australia, August 1991. Morgan Kaufman.
M. Fisher. A Normal Form for First-Order Temporal Formulae. In Proceedings of Eleventh International Conference on Automated Deduction (CADE),volume 607 of Lecture Notes in Computer Science, Saratoga Springs, New York, June 1992. Springer-Verlag.
A. Frisch and R. Scherl. A constraint logic approach to modal deduction. Lecture Notes in Computer Science, 478: 234–250, 1990.
B. T. Hailpern. Verifying Concurrent Processes Using Temporal Logic, volume 129 of Lecture Notes in Computer Science. Springer-Verlag, 1982.
W. W. McCune. OTTER 2.0 Users Guide. Argonne National Laboratory, 9700
South Cass Avenue, Argonne, Illinois 60439-4801, March 1990. ANL-90/9.
Z. Manna and A. Pnueli. Verification of Concurrent Programs: The Temporal Frame work. In Robert S. Boyer and J. Strother Moore, editors, The Correctness Problem in Computer Science, pages 215–273. Academic Press, London, 1981.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1992.
A. Nonnengart. Resolution-Based Calculi for Modal and Temporal Logics. In M. A. McRobbie and J. K. Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE), volume 1104 of Lecture Notes in Artificial Intelligence, pages 598–612, New Brunswick, New Jersey, July/August 1996. Springer-Verlag.
H.-J. Ohlbach. A Resolution Calculus for Modal Logics. Lecture Notes in Computer Science, 310: 500–516, May 1988.
S. Owicki and L. Lamport. Proving Liveness Properties of Concurrent Programs. ACM Transactions on Programming Languages and Systems, 4 (3): 455–495, July 1982.
M. Peim. Propositional Temporal Resolution Over Labelled Transition Systems. Unpublished Technical Note, Department of Computer Science, University of Manchester, 1994.
G. L. Peterson. Myths about the Mutual Exclusion Problem. Information Processing Letters, 12 (3): 115–116, 1981.
A. Pnueli. In Transition From Global to Modular Temporal Reasoning about Programs. In Krysztof Apt, editor, Logics and Models of Concurrent Systems, pages 123–144, La Colle-sur-Loup, France, October 1984. NATO, Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Dixon, C. (2000). Using Otter for Temporal Resolution. In: Barringer, H., Fisher, M., Gabbay, D., Gough, G. (eds) Advances in Temporal Logic. Applied Logic Series, vol 16. Springer, Dordrecht. https://doi.org/10.1007/978-94-015-9586-5_8
Download citation
DOI: https://doi.org/10.1007/978-94-015-9586-5_8
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5389-3
Online ISBN: 978-94-015-9586-5
eBook Packages: Springer Book Archive