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 firstorder 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.
CITATION STYLE
Degtyarev, A., Fisher, M., & Konev, B. (2003). Monodic temporal resolution. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2741, pp. 397–411). Springer Verlag. https://doi.org/10.1007/978-3-540-45085-6_35
Mendeley helps you to discover research relevant for your work.