Anatoli Degtyarev
Skip Abstract Section
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.
- 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.]]Google Scholar
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Börger, E., Grädel, E., and Gurevich, Y. 1997. The Classical Decision Problem. Springer, Berlin, Germany.]]Google Scholar
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- Degtyarev, A., Fisher, M., and Lisitsa, A. 2002b. Equality and monodic first-order temporal logic. Studia Logica 72, 2, 147--156.]]Google ScholarCross Ref
- 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.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]] Google ScholarDigital Library
- Fisher, M. 1997. A normal form for temporal logics and its applications in theorem proving and execution. J. Logic Computat. 7, 4, 429--456.]]Google ScholarCross Ref
- Fisher, M., Dixon, C., and Peim, M. 2001. Clausal temporal resolution. ACM Trans. Computat. Logic 2, 1, 12--56.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Gallier, H. 1986. Logic for Computer Science. Harper and Row, New York, NY.]]Google Scholar
- 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.]] Google ScholarDigital Library
- Hodkinson, I. 2002. Monodic packed fragment with equality is decidable. Studia Logica 72, 185--197.]]Google ScholarCross Ref
- Hodkinson, I., Wolter, F., and Zakharyaschev, M. 2000. Decidable fragments of first-order temporal logics. Ann. Pure Appl. Logic 106, 85--134.]]Google ScholarCross Ref
- Holzmann, G. J. 1997. The model checker Spin. IEEE Trans. Softw. Eng. 23, 5, 279--295.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- 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.]] Google ScholarDigital Library
- Kaivola, R. 1995. Axiomatising linear-time mu-calculus. In Proceedings of Concur'95.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- 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.]]Google Scholar
- Konev, B., Degtyarev, A., Dixon, C., Fisher, M., and Hustadt, U. 2005. Mechanizing first-order temporal resolution. Inform. Computat. 199, 1--2, 55--86.]]Google ScholarCross Ref
- Kontchakov, R., Lutz, C., Wolter, F., and Zakharyaschev, M. 2004. Temporalising tableaux. Studia Logica, 76, 1, 91--134.]]Google ScholarCross Ref
- Manna, Z. and Pnueli, A. 1992. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Berlin, Germany.]] Google ScholarDigital Library
- Maslov, S. 1968. The inverse method for establishing deducibility for logical calculi. Trudy Math. Inst. Steklov XCVIII, 22--25. (English translation AMS 1971.)]]Google Scholar
- Merz, S. 1992. Decidability and incompleteness results for first-order temporal logic of linear time. J. Appl. Non-Class. Logics 2, 139--156.]]Google ScholarCross Ref
- 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.]]Google Scholar
- Plaisted, D. and Greenbaum, S. 1986. A structure-preserving clause form transformation. J. Symbol. Computat. 2, 3 (Sept.), 293--304.]] Google ScholarDigital Library
- Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science. 46--57.]]Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
- Szalas, A. and Holenderski, L. 1988. Incompleteness of first-order temporal logic with until. Theoret. Comput. Sci. 57, 317--325.]] Google ScholarDigital Library
- 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.)]]Google Scholar
- Wolper, P. 1982. Synthesis of communicating processes from temporal logic specifications. Ph.D. dissertation. Stanford University, Stanford, CA.]] Google ScholarDigital Library
- Wolter, F. and Zakharyaschev, M. 2001. Decidable fragments of first-order modal logics. J. Symbol. Logic 66, 1415--1438.]]Google ScholarCross Ref
- Wolter, F. and Zakharyaschev, M. 2002a. Axiomatizing the monodic fragment of first-order temporal logic. Ann. Pure Appl. logic 118, 133--145.]]Google Scholar
- 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.]] Google ScholarDigital Library
Index Terms
- Monodic temporal resolution
Recommendations
Clausal temporal resolution
In this article, we examine how clausal resolution can be applied to a specific, but widely used, nonclassical logic, namely discrete linear temporal logic. Thus, we first define a normal form for temporal formulae and show how arbitrary temporal ...
Implementing a fair monodic temporal logic prover
Practical Aspects of Automated ReasoningMonodic first-order temporal logic is a fragment of first-order temporal logic for which sound and complete calculi have been devised. One such calculus is ordered fine-grained resolution with selection, which is implemented in the theorem prover TeMP. ...
Theorem Proving Modulo
AbstractDeduction modulo is a way to remove computational arguments from proofs by reasoning modulo a congruence on propositions. Such a technique, issued from automated theorem proving, is of general interest because it permits one to separate ...
Comments