Abstract
First-order temporal logic is a concise and powerful notation, with many potential applications in both Computer Science and Artificial Intelligence. While the full logic is highly complex, recent work on monodic first-order temporal logics have identified important enumerable and even decidable fragments. In this paper we present the first resolution-based calculus for monodic first-order temporal logic. Although the main focus of the paper is on establishing completeness results, we also consider implementation issues and define a basic loop-search algorithm that may be used to guide the temporal resolution system.
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
Degtyarev, A., Fisher, M.: Towards first-order temporal resolution. In: Baader, F., Brewka, G., Eiter, T. (eds.) KI 2001. LNCS (LNAI), vol. 2174, pp. 18–32. Springer, Heidelberg (2001)
Degtyarev, A., Fisher, M., Konev, B.: A simplified clausal resolution procedure for propositional linear-time temporal logic. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 85–99. Springer, Heidelberg (2002)
Degtyarev, A., Fisher, M., Konev, B.: Monodic temporal resolution. Technical Report ULCS-03-001, University of Liverpool, Department of Computer Science (2003), http://www.csc.liv.ac.uk/research/
Dixon, C.: Search strategies for resolution in temporal logics. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol. 1104, pp. 673–687. Springer, Heidelberg (1996)
Fisher, M.: A resolution method for temporal logic. In: Myopoulos, J., Reiter, R. (eds.) Proc. IJCAI 1991, pp. 99–104. Morgan Kaufmann, San Francisco (1991)
Fisher, M.: A normal form for temporal logics and its applications in theorem proving and execution. Journal of Logic and Computation 7(4), 429–456 (1997)
Fisher, M., Dixon, C., Peim, M.: Clausal temporal resolution. ACM Transactions on Computational Logic 2(1), 12–56 (2001)
Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable fragments of first-order temporal logics. Annals of Pure and Applied Logic 106, 85–134 (2000)
Holzmann, G.J.: The model checker Spin. IEEE Trans. on Software Engineering 23(5), 279–295 (1997)
Kontchakov, R., Lutz, C., Wolter, F., Zakharyaschev, M.: Temporalising tableaux. Studia Logica (to appear)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)
Merz, S.: Decidability and incompleteness results for first-order temporal logic of linear time. Journal of Applied Non-Classical Logics 2, 139–156 (1992)
Pnueli, A.: The Temporal Logic of Programs. In: Proceedings of the Eighteenth Symposium on the Foundations of Computer Science (1977)
Szalas, A., Holenderski, L.: Incompleteness of First-Order Temporal Logic with Until. Theoretical Computer Science 57, 317–325 (1988)
Wolter, F., Zakharyaschev, M.: Axiomatizing the monodic fragment of first-order temporal logic. Annals of Pure and Applied logic 118, 133–145 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Degtyarev, A., Fisher, M., Konev, B. (2003). Monodic Temporal Resolution. In: Baader, F. (eds) Automated Deduction – CADE-19. CADE 2003. Lecture Notes in Computer Science(), vol 2741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45085-6_35
Download citation
DOI: https://doi.org/10.1007/978-3-540-45085-6_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40559-7
Online ISBN: 978-3-540-45085-6
eBook Packages: Springer Book Archive