Abstract
Both proof, via clausal resolution, and execution, via the imperative future approach, depend on the use of a normal form for temporal formulae. While the systems developed have centred around the use of an unrestricted normal form, we here consider a Horn clause-like version of the normal form and its effect on both execution and resolution. This refined normal form is as expressive as the original, and represents a natural way to describe systems, yet allows both execution and resolution to be implemented more efficiently in practice.
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
M. Abadi. Temporal-Logic Theorem Proving. PhD thesis, Department of Computer Science, Stanford University, March 1987.
H. Barringer, M. Fisher, D. Gabbay, and A. Hunter. Meta-Reasoning in Executable Temporal Logic. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR), April 1991.
H. Barringer, M. Fisher, D. Gabbay, G. Gough, and R. Owens. METATEM: An Introduction. Formal Aspects of Computing, 7 (5): 533–549, 1995.
H. Barringer, M. Fisher, D. Gabbay, R. Owens, and M. Reynolds, editors. The Imperative Future: Principles of Executable Temporal Logics. Research Studies Press, Chichester, United Kingdom, 1996.
C. L. Chang. The Unit Proof and the Input Proof in Theorem Proving. ACM Journal, 17: 698–707, 1970.
C. Dixon. Search Strategies for Resolution in Temporal Logics. In Proceedings of the Thirteenth International Conference on Automated Deduction (CADE), volume 1104 of Lecture Notes in Computer Science, New Brunswick, New Jersey, July/August 1996.
E. A. Emerson and A. P. Sistla. Deciding full branching time logic. Information and Control, 61: 175–201, 1984.
L. Fariñas del Cerro and M. Penttonen, editors. Intensional Logics for Programming. Oxford University Press, 1992.
M. Finger, P. McBrien, and R. Owens. Databases and Executable Temporal Logic. In Proceedings of the ESPRIT Conference, November 1991.
M. Finger, M. Fisher, and R. Owens. METATEM at Work: Modelling Reactive Systems Using Executable Temporal Logic. In Sixth International Conference on Industrial and Engineering Applications of Artificial Intelligence and Expert Systems (IEA/AIE),Edinburgh, U.K., June 1993. Gordon and Breach Publishers.
M. Fisher. A Resolution Method for Temporal Logic. In Proceedings of the Twelfth International Joint Conference on Artificial Intelligence, Sydney, Australia, 1991.
M. Fisher. A Survey of Concurrent METATEM — The Language and its Applications. In First International Conference on Temporal Logic (ICTL), Bonn, Germany, July 1994.
M. Fisher. A Normal Form for Temporal Logic and its Application in TheoremProving and Execution. Journal of Logic and Computation, 7 (4), August 1997.
M. Fisher and R. Owens, editors. Executable Modal and Temporal Logics, volume 897 of Lecture Notes in Artificial Intelligence. Springer-Verlag, February 1995.
D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. The Temporal Analysis of Fairness. In Proceedings of the Seventh Symposium on the Principles of Programming Languages, 1980.
N. D. Jones and W. T. Lasser. Complete problems for deterministic polynomial time. Theoretical Computer Science, 3: 107–117, 1977.
R. McNaughton. Testing and Generating Infinite Sequences by a Finite Automaton. Information and Control, 9: 521–530, 1966.
B. Moszkowski. Executing Temporal Logic Programs. Cambridge University Press, Cambridge, U.K., 1986.
M. Peim. Propositional Temporal Resolution Over Labelled Transition Systems. Unpublished Technical Note, Department of Computer Science, University of Manchester, 1994.
J. A. Robinson. A Machine—Oriented Logic Based on the Resolution Principle. ACM Journal, 12 (1): 23–41, January 1965.
S. Safra and M. Y. Vardi. On w-Automata and Temporal Logic. In STOC,pages 127–137, Seattle, Washington, May 1989. ACM.
A. P. Sistla and E. M. Clarke. Complexity of propositional linear temporal logics. ACM Journal, 32 (3): 733–749, July 1985.
M. Y. Vardi and P. Wolper. Automata-theoretic Techniques for Modal Logics of Programs. Journal of Computer and System Sciences, 32 (2): 183–219, April 1986.
P. Wolper. The Tableau Method for Temporal Logic: An overview. Logique et Analyse, 110–111:119–136, June-Sept 1985.
L. Wos, D. Carson, and G. Robinson. The Unit Preference Strategy in Theorem Proving. In Proceedings of AFIPS Fall Joint Computer Conference. Thompson Book Co., 1964.
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., Fisher, M., Reynolds, M. (2000). Execution and Proof in a Horn-Clause Temporal Logic. 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_21
Download citation
DOI: https://doi.org/10.1007/978-94-015-9586-5_21
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-5389-3
Online ISBN: 978-94-015-9586-5
eBook Packages: Springer Book Archive