skip to main content
article

Monodic temporal resolution

Published: 01 January 2006 Publication History

Abstract

Until recently, First-Order Temporal Logic (FOTL) has been only partially understood. While it is well known that the full logic has no finite axiomatisation, a more detailed analysis of fragments of the logic was not previously available. However, a breakthrough by Hodkinson et al., identifying a finitely axiomatisable fragment, termed the monodic fragment, has led to improved understanding of FOTL. Yet, in order to utilise these theoretical advances, it is important to have appropriate proof techniques for this monodic fragment.In this paper, we modify and extend the clausal temporal resolution technique, originally developed for propositional temporal logics, to enable its use in such monodic fragments. We develop a specific normal form for monodic formulae in FOTL, and provide a complete resolution calculus for formulae in this form. Not only is this clausal resolution technique useful as a practical proof technique for certain monodic classes, but the use of this approach provides us with increased understanding of the monodic fragment. In particular, we here show how several features of monodic FOTL can be established as corollaries of the completeness result for the clausal temporal resolution method. These include definitions of new decidable monodic classes, simplification of existing monodic classes by reductions, and completeness of clausal temporal resolution in the case of monodic logics with expanding domains, a case with much significance in both theory and practice.

References

[1]
Artale, A. and Franconi, E. 2004. Temporal description logics. In Handbook of Temporal Reasoning in Artificial Intelligence, M. Fisher, D. M. Gabbay, and L. Vila, Eds. Elsevier, Amsterdam, The Netherlands.]]
[2]
Artale, A., Franconi, E., Wolter, F., and Zakharyaschev, M. 2002. A temporal description logic for reasoning over conceptual schemas and queries. In Proceedings of JELIA'02. Lecture Notes in Computer Science, vol. 2424. Springer, Berlin, Germany, 98--110.]]
[3]
Bachmair, L. and Ganzinger, H. 2001. Resolution theorem proving. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, Amsterdam, The Netherlands, Chapter 2, 19--99.]]
[4]
Börger, E., Grädel, E., and Gurevich, Y. 1997. The Classical Decision Problem. Springer, Berlin, Germany.]]
[5]
Degtyarev, A. and Fisher, M. 2001. Towards first-order temporal resolution. In KI 2001, Proceedings. Lecture Notes in Computer Science, vol. 2174. Springer, Berlin, Germany, 18--32.]]
[6]
Degtyarev, A., Fisher, M., and Konev, B. 2002a. A simplified clausal resolution procedure for propositional linear-time temporal logic. In Tableaux 2002, Proceedings. Lecture Notes in Computer Science, vol. 2381. Springer, Berlin, Germany, 85--99.]]
[7]
Degtyarev, A., Fisher, M., and Konev, B. 2003a. Handling equality in monodic temporal resolution. In Proceedings of 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Lecture Notes in Computer Science, vol. 2850. Springer-Verlag, Berlin, Germany, 214--228.]]
[8]
Degtyarev, A., Fisher, M., and Konev, B. 2003b. Monodic temporal resolution. In Proc. CADE-19. Lecture Notes in Artificial Intelligence, vol. 2741. Springer, Berlin, Germany, 397--411.]]
[9]
Degtyarev, A., Fisher, M., and Lisitsa, A. 2002b. Equality and monodic first-order temporal logic. Studia Logica 72, 2, 147--156.]]
[10]
Dixon, C. 1996. Search strategies for resolution in temporal logics. In Proceedings of the CADE-13. Lecture Notes in Artificial Intelligence, vol. 1104. Springer, Berlin, Germany, 673--687.]]
[11]
Fermüller, C., Leitsch, A., Hustadt, U., and Tammet, T. 2001. Resolution decision procedures. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, Amsterdam, The Netherlands, Volume II, Chapter 25, 1791--1850.]]
[12]
Fisher, M. 1991. A resolution method for temporal logic. In Proceedings of IJCAI'91, J. Myopoulos and R. Reiter, Eds. Morgan Kaufman, San Francisco, CA, 99--104.]]
[13]
Fisher, M. 1992. A normal form for first-order temporal formulae. In Proceedings of the 11th International Conference on Automated Deduction, D. Kapur, Ed. Lecture Notes in Artificial Intelligence, vol. 607. Springer Verlag, Berlin, Germany, 370--384.]]
[14]
Fisher, M. 1997. A normal form for temporal logics and its applications in theorem proving and execution. J. Logic Computat. 7, 4, 429--456.]]
[15]
Fisher, M., Dixon, C., and Peim, M. 2001. Clausal temporal resolution. ACM Trans. Computat. Logic 2, 1, 12--56.]]
[16]
Fisher, M. and Ghidini, C. 2002. The ABC of rational agent programming. In Proceedings of the First International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS). ACM Press, New York, NY, 849--856.]]
[17]
Fisher, M. and Lisitsa, A. 2003. Deductive verification of cache coherence protocols. In Proceedings of 3rd International Workshop on Automated Verification of Critical Systems (AVoCS 2003; Southampton, U.K.). 177--186.]]
[18]
Gabbay, D. 1987. Declarative past and imperative future: Executive temporal logic for interactive systems. In Proceedings on Colloquium on Temporal Logic and Specification, B. Banieqbal, H. Barringer, and A. Pnueli, Eds. Lecture Notes in Computer Science, vol. 398. Springer Verlag, Berlin, Germany, 402--450.]]
[19]
Gabelaia, D., Kontchakov, R., Kurucz, A., Wolter, F., and Zakharyaschev, M. 2003. On the computational complexity of spatio-temporal logics. In Proceedings of the 16th International FLAIRS Conference. AAAI Press, Menlo Park, CA, 460--464.]]
[20]
Gallier, H. 1986. Logic for Computer Science. Harper and Row, New York, NY.]]
[21]
Ganzinger, H. and De Nivelle, H. 1999. A superposition decision procedure for the guarded fragment with equality. In Proceedings of the 14th IEEE Symposium on Logic in Computer Science. 295--305.]]
[22]
Hodkinson, I. 2002. Monodic packed fragment with equality is decidable. Studia Logica 72, 185--197.]]
[23]
Hodkinson, I., Wolter, F., and Zakharyaschev, M. 2000. Decidable fragments of first-order temporal logics. Ann. Pure Appl. Logic 106, 85--134.]]
[24]
Holzmann, G. J. 1997. The model checker Spin. IEEE Trans. Softw. Eng. 23, 5, 279--295.]]
[25]
Hustadt, U. and Konev, B. 2003. TRP++ 2.0: A temporal resolution prover. In Proceedings of CADE-19. Lecture Notes in Artificial Intelligence, vol. 2741. Springer, Berlin, Germany, 274--278.]]
[26]
Hustadt, U., Konev, B., Voronkov, A., and Riazanov, A. 2004. TeMP: A temporal monodic prover. Tech. rep. ULCS-04-004. Department of Computer Science, University of Liverpool, Liverpool, U.K. Also published in Proceedings of IJCAR 2004. Lecture Notes in Artificial Intelligence, vol. 3097. Springer, Berlin, Germany, 326--330.]]
[27]
Hustadt, U. and Schmidt, R. A. 1999. Maslov's class K revisited. In Proceedings of the 16th International Conference on Automated Deduction (CADE-16), H. Ganzinger, Ed. Lecture Notes in Artificial Intelligence, vol. 1632. Springer, Berlin, Germany, 172--186.]]
[28]
Kaivola, R. 1995. Axiomatising linear-time mu-calculus. In Proceedings of Concur'95.]]
[29]
Kesten, Y. and Pnueli, A. 1995. A complete proof system for QPTL. In Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, Los Alamitos, CA, 2--12.]]
[30]
Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U. 2003. Towards the implementation of first-order temporal resolution: The expanding domain case. In Proceedings TIME-ICTL'03. IEEE Computer Society Press, Los Alamitos, CA, 72--82.]]
[31]
Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U. 2005. Mechanizing first-order temporal resolution. Inform. Computat. 199, 1--2, 55--86.]]
[32]
Kontchakov, R., Lutz, C., Wolter, F., and Zakharyaschev, M. 2004. Temporalising tableaux. Studia Logica, 76, 1, 91--134.]]
[33]
Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin, Germany.]]
[34]
Maslov, S. 1968. The inverse method for establishing deducibility for logical calculi. Trudy Math. Inst. Steklov XCVIII, 22--25. (English translation AMS 1971.)]]
[35]
Merz, S. 1992. Decidability and incompleteness results for first-order temporal logic of linear time. J. Appl. Non-Class. Logics 2, 139--156.]]
[36]
Nonnengart, A. and Weidenbach, C. 2001. Computing small clause normal forms. In Handbook of Automated Reasoning, A. Robinson and A. Voronkov, Eds. Elsevier, Amsterdam, The Netherlands, Chapter 6, 335--370.]]
[37]
Plaisted, D. and Greenbaum, S. 1986. A structure-preserving clause form transformation. J. Symbol. Computat. 2, 3 (Sept.), 293--304.]]
[38]
Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science. 46--57.]]
[39]
Riazanov, A. and Voronkov, A. 2001. Vampire 1.1 (system description). In Proceedings of IJCAR 2001. Lecture Notes in Computer Science, vol. 2083. Springer, Berlin, Germany.]]
[40]
Szalas, A. and Holenderski, L. 1988. Incompleteness of first-order temporal logic with until. Theoret. Comput. Sci. 57, 317--325.]]
[41]
Tseitin, G. 1983. On the complexity of derivations in propositional calculus. In Automation of Reasoning (Classical Papers on Computational Logic), J. Siekmann and G. Wrightson, Eds. Springer Verlag, Berlin, Germany, vol. 2, 466--483. (Original article (in Russian) appeared in 1968.)]]
[42]
Wolper, P. 1982. Synthesis of communicating processes from temporal logic specifications. Ph.D. dissertation. Stanford University, Stanford, CA.]]
[43]
Wolter, F. and Zakharyaschev, M. 2001. Decidable fragments of first-order modal logics. J. Symbol. Logic 66, 1415--1438.]]
[44]
Wolter, F. and Zakharyaschev, M. 2002a. Axiomatizing the monodic fragment of first-order temporal logic. Ann. Pure Appl. logic 118, 133--145.]]
[45]
Wolter, F. and Zakharyaschev, M. 2002b. Qualitative spatio-temporal representation and reasoning: A computational perspective. In Exploring Artificial Intelligence in the New Millenium. Morgan Kaufmann, San Francisco, CA, 175--216.]]

Cited By

View all
  • (2023)Performance Implication of Tensor Irregularity and Optimization for Distributed Tensor DecompositionACM Transactions on Parallel Computing10.1145/358031510:2(1-27)Online publication date: 20-Jun-2023
  • (2023)PEDM: A Multi-task Learning Model for Persona-aware Emoji-embedded Dialogue GenerationACM Transactions on Multimedia Computing, Communications, and Applications10.1145/357181919:3s(1-21)Online publication date: 24-Feb-2023
  • (2023)Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal LogicStudia Logica10.1007/s11225-023-10052-7111:6(979-1014)Online publication date: 1-Dec-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic
ACM Transactions on Computational Logic  Volume 7, Issue 1
January 2006
198 pages
ISSN:1529-3785
EISSN:1557-945X
DOI:10.1145/1119439
Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2006
Published in TOCL Volume 7, Issue 1

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. Temporal logic
  2. automated theorem proving
  3. resolution

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)14
  • Downloads (Last 6 weeks)0
Reflects downloads up to 13 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)Performance Implication of Tensor Irregularity and Optimization for Distributed Tensor DecompositionACM Transactions on Parallel Computing10.1145/358031510:2(1-27)Online publication date: 20-Jun-2023
  • (2023)PEDM: A Multi-task Learning Model for Persona-aware Emoji-embedded Dialogue GenerationACM Transactions on Multimedia Computing, Communications, and Applications10.1145/357181919:3s(1-21)Online publication date: 24-Feb-2023
  • (2023)Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal LogicStudia Logica10.1007/s11225-023-10052-7111:6(979-1014)Online publication date: 1-Dec-2023
  • (2021)Reasoning about Petri Nets: A Calculus Based on Resolution and Dynamic LogicACM Transactions on Computational Logic10.1145/344165522:2(1-22)Online publication date: 15-May-2021
  • (2021)Parameterized verification of leader/follower systems via first-order temporal logicFormal Methods in System Design10.1007/s10703-022-00390-y58:3(440-468)Online publication date: 1-Nov-2021
  • (2021)Theorem Proving Using Clausal Resolution: From Past to PresentReachability Problems10.1007/978-3-030-89716-1_2(19-27)Online publication date: 25-Oct-2021
  • (2018)Temporal logic of common knowledge and its resolution-based proof methodJournal of Intelligent & Fuzzy Systems10.3233/JIFS-17988(1-16)Online publication date: 21-Aug-2018
  • (2017)Horn Fragments of the Halpern-Shoham Interval Temporal LogicACM Transactions on Computational Logic10.1145/310590918:3(1-39)Online publication date: 11-Aug-2017
  • (2016)On temporal logics with data variable quantificationsInformation and Computation10.1016/j.ic.2016.08.002251:C(104-139)Online publication date: 1-Dec-2016
  • (2016)AAL and Static Conflict Detection in PolicyCryptology and Network Security10.1007/978-3-319-48965-0_22(367-382)Online publication date: 14-Nov-2016
  • Show More Cited By

View Options

Login options

Full Access

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media