Jose Gaintzarain
Skip Abstract Section
Abstract
In this article, we present a declarative propositional temporal logic programming language called TeDiLog that is a combination of the temporal and disjunctive paradigms in logic programming. TeDiLog is, syntactically, a sublanguage of the well-known Propositional Linear-time Temporal Logic (PLTL). TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. The operational semantics of TeDiLog relies on a restriction of the invariant-free temporal resolution procedure for PLTL that was introduced by Gaintzarain et al. in [2013]. We define a fixpoint semantics that captures the reverse (bottom-up) operational mechanism and prove its equivalence with the logical semantics. We also provide illustrative examples and comparison with other proposals.
- Abadi, M. and Manna, Z. 1987. Temporal logic programming. In Proceedings of the International Symposium on Logic Programming. IEEE Computer Society Press, Los Alamitos, CA, 4--16.Google Scholar
- Abadi, M. and Manna, Z. 1989. Temporal logic programming. J. Symbolic Comput. 8, 3, 277--295. Google ScholarDigital Library
- Aguado, F., Cabalar, P., Perez, G., and Vidal, C. 2008. Strongly equivalent temporal logic programs. In Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA'08). Lecture Notes in Computer Science, vol. 5293, Springer, 8--20. Google ScholarDigital Library
- Aguado, F., Cabalar, P., Perez, G., and Vidal, C. 2011. Loop formulas for splitable temporal logic programs. In Proceedings of the 11th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'11). Lecture Notes in Computer Science, vol. 6645, Springer, 80--92. Google ScholarDigital Library
- Balbiani, P., Farinas Del Cerro, L., and Herzig, A. 1988. Declarative semantics for modal logic programs. In Proceedings of the International Conference on 5th Generation Computer Systems (FGCS'88). OHMSHA Ltd. Tokyo and Springer, 507--514.Google Scholar
- Barringer, H., Fisher, M., Gabbay, D. M., Gough, G., and Owens, R. 1989. METATEM: A framework for programming in temporal logic. In Proceedings of the REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness. Lecture Notes in Computer Science, vol. 430, Springer, 94--129. Google ScholarDigital Library
- Baudinet, M. 1988. On the semantics of temporal logic programming. Tech. rep. CS-TR-88-1203. Department of Computer Science, Stanford University, CA. ftp://reports.stanford.edu/pub/cstr/reports/cs/tr/88/1203/CS-TR-88-1203.pdf. Google ScholarDigital Library
- Baudinet, M. 1989a. Logic programming semantics: Techniques and applications. Ph.D. dissertation. Department of Computer Science, Stanford University, CA. Google ScholarDigital Library
- Baudinet, M. 1989b. Temporal logic programming is complete and expressive. In Proceedings of the 16th Annual ACM Symposium on Principles of Programming Languages (POPL'89). ACM Press, New York, 267--280. Google ScholarDigital Library
- Baudinet, M. 1992. A simple proof of the completeness of temporal logic programming. In Intensional Logics for Programming. Oxford University Press, 51--83.Google Scholar
- Baudinet, M. 1995. On the expressiveness of temporal logic programming. Inf. Comput. 117, 2, 157--180. Google ScholarDigital Library
- Brunnler, K. and Lange, M. 2008. Cut-free sequent systems for temporal logic. J. Logic Algebraic Program. 76, 2, 216--225.Google ScholarCross Ref
- Brzoska, C. 1991. Temporal logic programming and its relation to constraint logic programming. In Proceedings of the International Symposium on Logic Programming (ISLP'91). MIT Press, 661--677.Google Scholar
- Brzoska, C. 1993. Temporal logic programming with bounded universal modality goals. In Proceedings of the 10th International Conference on Logic Programming (ICLP'93). MIT Press, 239--256. Google ScholarDigital Library
- Brzoska, C. 1995a. Temporal logic programming in dense time. In Proceedings of the International Logic Programming Symposium (ILPS'95). MIT Press, 303--317.Google Scholar
- Brzoska, C. 1995b. Temporal logic programming with metric and past operators. In Proceedings of the Workshop on Executable Modal and Temporal Logics. Lecture Notes in Computer Science, vol. 897, Springer, 21--39. Google ScholarDigital Library
- Brzoska, C. 1998. Programming in metric temporal logic. Theor. Comput. Sci. 202, 1--2, 55--125. Google ScholarDigital Library
- Brzoska, C. and Schafer, K. 1995. Temporal logic programming applied to image sequence evaluation. In Logic Programming: Formal Methods and Practical Applications. Elsevier Science, 381--395.Google Scholar
- Cau, A., Zedan, H., Coleman, N., and Moszkowski, B. C. 1996. Using itl and tempura for large-scale specification and simulation. In Proceedings of the 4th Euromicro Workshop on Parallel and Distributed Processing (PDP'96). IEEE Computer Society Press, Los Alamitos, CA, 493--500. Google ScholarDigital Library
- Clarke, E. M., Emerson, E. A., and Sistla, A. P. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8, 2, 244--263. Google ScholarDigital Library
- Clarke, E. M., Grumberg, O., and Peled, D. 2001. Model Checking. MIT Press.Google Scholar
- Dixon, C. and Fisher, M. 1998. The set of support strategy in temporal resolution. In Proceedings of the 5th International Workshop on Temporal Representation and Reasoning (TIME'98). IEEE Computer Society Press, Los Alamitos, CA, 113--120. Google ScholarDigital Library
- Dixon, C., Fisher, M., and Konev, B. 2006. Is there a future for deductive temporal verification? In Proceedings of the 13th International Symposium on Temporal Representation and Reasoning (TIME'06). IEEE Computer Society Press, Los Alamitos, CA, 11--18. Google ScholarDigital Library
- Dixon, C., Fisher, M., and Reynolds, M. 2000. Execution and proof in a horn-clause temporal logic. In Advances in Temporal Logic. Kluwer Academic Publishers, 413--433.Google Scholar
- Duan, Z., Yang, X., and Koutny, M. 2005. Semantics of framed temporal logic programs. In Proceedings of the 21st International Conference on Logic Programming (ICLP'05). Lecture Notes in Computer Science, vol. 3668, Springer, 356--370. Google ScholarDigital Library
- Duan, Z., Yang, X., and Koutny, M. 2008. Framed temporal logic programming. Sci. Comput. Program. 70, 1, 31--61. Google ScholarDigital Library
- Farinas Del Cerro, L. 1986. MOLOG: A system that extends prolog with modal logic. New Generation Comput. 4, 35--50. Google ScholarDigital Library
- Fisher, M. 1991. A resolution method for temporal logic. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI'91). Morgan Kaufmann, 99--104. Google ScholarDigital Library
- Fisher, M. 1992. A normal form for first-order temporal formulae. In Proceedings of the 11th International Conference on Automated Deduction (CADE'92). Lecture Notes in Computer Science, vol. 607, Springer, 370--384. Google ScholarDigital Library
- Fisher, M. 1993. Concurrent metatem--A language for modeling reactive systems. In Proceedings of the Conference on Parallel Architectures and Languages, Europe (PARLE'93). Lecture Notes in Computer Science, vol. 694, Springer, 185--196. Google ScholarDigital Library
- Fisher, M. 1997. Implementing bdi-like systems by direct execution. In Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI'97). Morgan Kaufmann, 316--321. Google ScholarDigital Library
- Fisher, M. 2011. An Introduction to Practical Formal Methods Using Temporal Logic. John Wiley and Sons, Ltd. Google ScholarDigital Library
- Fisher, M., Dixon, C., and Peim, M. 2001. Clausal temporal resolution. ACM Trans. Comput. Logic 2, 1, 12--56. Google ScholarDigital Library
- Fisher, M. and Ghidini, C. 2010. Executable specifications of resource-bounded agents. Auton. Agents Multi-Agent Syst. 21, 3, 368--396. Google ScholarDigital Library
- Fruhwirth, T. W. 1994. Annotated constraint logic programming applied to temporal reasoning. In Proceedings of the 6th International Symposium on Programming Language Implementation and Logic Programming (PLILP'94). Lecture Notes in Computer Science, vol. 844, Springer, 230--243. Google ScholarDigital Library
- Fruhwirth, T. W. 1995. Temporal logic and annotated constraint logic programming. In Proceedings of the Workshop on Executable Modal and Temporal Logics. Lecture Notes in Computer Science, vol. 897, Springer, 58--68. Google ScholarDigital Library
- Fruhwirth, T. W. 1996. Temporal annotated constraint logic programming. J. Symbolic Comput. 22, 5/6, 555--583. Google ScholarDigital Library
- Fujita, M., Kono, S., Tanaka, H., and Moto-Oka, T. 1986. Tokio: Logic programming language based on temporal logic and its compilation to prolog. In Proceedings of the 3rd International Conference on Logic Programming (ICLP'86). Lecture Notes in Computer Science, vol. 225, Springer, 695--709. Google ScholarDigital Library
- Gabbay, D. M. 1987a. The declarative past and imperative future: Executable temporal logic for interactive systems. In Proceedings of the Colloquium on Temporal Logic in Specification. Lecture Notes in Computer Science, vol. 398, Springer, 409--448. Google ScholarDigital Library
- Gabbay, D. M. 1987b. Modal and temporal logic programming. In Temporal Logics and Their Application. Academic Press, 197--237. Google ScholarDigital Library
- Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., and Orejas, F. 2009. Dual systems of tableaux and sequents for pltl. J. Logic Algebraic Program. 78, 8, 701--722.Google ScholarCross Ref
- Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., and Orejas, F. 2013. Invariant-free clausal temporal resolution. J. Autom. Reason. 50, 1, 1--49. Google ScholarDigital Library
- Gaintzarain, J. and Lucio, P. 2009. A new approach to temporal logic programming. In Proceedings of the 9th Spanish Conference on Programming and Languages (PROLE'09). 341--350. http://www.sistedes.es/ficheros/actas-conferencias/PROLE/2009.pdf.Google Scholar
- Gergatsoulis, M. 2001. Temporal and modal logic programming languages. In Encyclopedia of Microcomputers, vol. 27, CRC Press, 393--408.Google Scholar
- Gergatsoulis, M., Rondogiannis, P., and Panayiotopoulos, T. 2000. Temporal disjunctive logic programming. New Generation Comput. 19, 1, 87--102. Google ScholarDigital Library
- Goranko, V., Kyrilov, A., and Shkatov, D. 2010. Tableau tool for testing satisfiability in ltl: Implementation and experimental analysis. In Proceedings of the 6th Workshop on Methods for Modalities. Electronic Notes in Theoretical Computer Science, vol. 262, Elsevier, 113--125. Google ScholarDigital Library
- Hrycej, T. 1988. Temporal prolog. In Proceedings of the 8th European Conference on Artificial Intelligence (ECAI'88). Pitmann Publishing, 296--301.Google ScholarDigital Library
- Hrycej, T. 1993. A temporal extension of prolog. J. Logic Program. 15, 1--2, 113--145. Google ScholarDigital Library
- Hustadt, U. and Schmidt, R. A. 1999. An empirical analysis of modal theorem provers. J. Applied Non-Classical Logics 9, 4, 479--522.Google ScholarCross Ref
- Hustadt, U. and Schmidt, R. A. 2002. Scientific benchmarking with temporal logic decision procedures. In Proceedings of the 8th International Conference on Principles and Knowledge Representation and Reasoning (KR'02). Morgan Kaufmann, 533--544.Google Scholar
- Kamp, J. A. W. 1968. Tense logic and the theory of linear order. Ph.D. dissertation. Department of Computer Science, University of California, Los Angeles, CA.Google Scholar
- Knaster, B. 1928. Un theorem sur les fonctions d'ensembles. Annales de la Societe Polonaise de Mathematique 6, 133--134.Google Scholar
- Kono, S. 1995. A combination of clausal and non clausal temporal logic programs. In Proceedings of the Workshop on Executable Modal and Temporal Logics. Lecture Notes in Computer Science, vol. 897, Springer, 40--57. Google ScholarDigital Library
- Kono, S., Aoyagi, T., Fujita, M., and Tanaka, H. 1985. Implementation of temporal logic programming language tokio. In Proceedings of the 4th Conference on Logic Programming (LP'85). Lecture Notes in Computer Science, vol. 221, Springer, 138--147. Google ScholarDigital Library
- Lloyd, J. W. 1984. Foundations of Logic Programming 1st Ed. Springer. Google ScholarDigital Library
- Lobo, J., Minker, J., and Rajasekar, A. 1992. Foundations of Disjunctive Logic Programming. MIT Press. Google ScholarDigital Library
- Merz, S. 1992. Decidability and incompleteness results for first-order temporal logics of linear time. J. Applied Non-Classical Logics 2, 2, 139--156.Google ScholarCross Ref
- Merz, S. 1995. Efficiently executable temporal logic programs. In Proceedings of the Workshop on Executable Modal and Temporal Logics. Lecture Notes in Computer Science, vol. 897, Springer, 69--85. Google ScholarDigital Library
- Moszkowski, B. C. 1986. Executing Temporal Logic Programs. Cambridge University Press. Google ScholarDigital Library
- Moszkowski, B. C. 1998. Compositional reasoning using interval temporal logic and tempura. In Proceedings of the International Symposium on Compositionality: The Significant Difference (COMPOS'97). Lecture Notes in Computer Science, vol. 1536, Springer, 439--464. Google ScholarDigital Library
- Nakamura, H., Nakai, M., Kono, S., Fujita, M., and Tanaka, H. 1989. Logic design assistance using temporal logic based language tokio. In Proceedings of the 8th Conference on Logic Programming (LP'89). Lecture Notes in Computer Science, vol. 485, Springer, 174--183.Google Scholar
- Nguyen, L. A. 2000. Constructing the least models for positive modal logic programs. Fundamenta Informaticae 42, 1, 29--60. Google ScholarDigital Library
- Nguyen, L. A. 2003. A fixpoint semantics and an sld-resolution calculus for modal logic programs. Fundamenta Informaticae 55, 1, 63--100. Google ScholarDigital Library
- Nguyen, L. A. 2006. Multimodal logic programming. Theor. Comput. Sci. 360, 1--3, 247--288. Google ScholarDigital Library
- Nguyen, L. A. 2009. Modal logic programming revisited. J. Applied Non-Classical Logics 19, 2, 167--181.Google ScholarCross Ref
- Orgun, M. A. 1991. Intensional logic programming. Ph.D. dissertation. Department of Computer Science, University of Victoria, British Columbia, Canada. Google ScholarDigital Library
- Orgun, M. A. 1994. Temporal and modal logic programming: An annotated bibliography. SIGART Bull. 5, 3, 52--59. Google ScholarDigital Library
- Orgun, M. A. 1995. Foundations of linear-time logic programming. Int. J. Comput. Math. 58, 3--4, 199--219.Google ScholarCross Ref
- Orgun, M. A. and Ma, W. 1994. An overview of temporal and modal logic programming. In Proceedings of the 1st International Conference on Temporal Logic (ICTL'94). Lecture Notes in Computer Science, vol. 827, Springer, 445--479. Google ScholarDigital Library
- Orgun, M. A. and Wadge, W. W. 1992. Towards a unified theory of intensional logic programming. J. Logic Program. 13, 4, 413--440. Google ScholarDigital Library
- Orgun, M. A. and Wadge, W. W. 1994. Extending temporal logic programming with choice predicates non-determinism. J. Logic Comput. 4, 6, 877--903.Google ScholarCross Ref
- Orgun, M. A., Wadge, W. W., and Du, W. 1993. Chronolog (Z): Linear-time logic programming. In Proceedings of the 5th International Conference on Computing and Information (ICCI'93). IEEE Computer Society Press, Los Alamitos, CA, 545--549. Google ScholarDigital Library
- Paech, B. 1988. Gentzen-systems for propositional temporal logics. In Proceedings of the 2nd Workshop on Computer Science Logic (CSL'88). Lecture Notes in Computer Science, vol. 385, Springer, 240--253. Google ScholarDigital Library
- Pliuskevicius, R. 1991. Investigation of finitary calculus for a discrete linear time logic by means of infinitary calculus. In Baltic Computer Science, selected papers. Lecture Notes in Computer Science, vol. 502, Springer, 504--528. Google ScholarDigital Library
- Pliuskevicius, R. 1992. Logical foundation for logic programming based on first order linear temporal logic. In Proceedings of the 1st and 2nd Russian Conference on Logic Programming (RCLP'92). Lecture Notes in Computer Science, vol. 592, Springer, 391--406. Google ScholarDigital Library
- Raffaeta, A. and Fruhwirth, T. W. 1999. Two semantics for temporal annotated constraint logic programming. In Proceedings of the 12th International Symposium on Languages for Intensional Programming (ISLIP'99). World Scientific Press, 126--140.Google Scholar
- Reichgelt, H. 1987. Semantics for reified temporal logic. In Advances in Artificial Intelligence. John Wiley and Sons, Ltd., 49--61. Google ScholarDigital Library
- Rondogiannis, P., Gergatsoulis, M., and Panayiotopoulos, T. 1997. Cactus: A branching-time logic programming language. In Proceedings of the 1st International Joint Conference on Qualitative and Quantitative Practical Reasoning (ECSQARU-FAPR'97). Lecture Notes in Computer Science, vol. 1244, Springer, 511--524. Google ScholarDigital Library
- Rondogiannis, P., Gergatsoulis, M., and Panayiotopoulos, T. 1998. Branching-time logic programming: The language cactus and its applications. Comput. Lang. 24, 3, 155--178. Google ScholarDigital Library
- Sakuragawa, T. 1986. Temporal prolog. Tech. rep. Kyoto University. http://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/99379/1/0586-16.pdf.Google Scholar
- Schoning, U. 1989. Logic for Computer Scientists. Birkhauser. Google ScholarDigital Library
- Shoham, Y. 1986. Reified temporal logics: Semantical and ontological considerations. In Proceedings of the 7th European Conference on Artificial Intelligence (ECAI'86). 183--190.Google Scholar
- Sistla, A. P. and Clarke, E. M. 1985. The complexity of propositional linear temporal logics. J. ACM 32, 3, 733--749. Google ScholarDigital Library
- Szalas, A. 1995. Temporal logic of programs: A standard approach. In Time and Logic. A Computational Approach, UCL Press Ltd., 1--50. Google ScholarDigital Library
- Szalas, A. and Holenderski, L. 1988. Incompleteness of first-order temporal logic with until. Theor. Comput. Sci. 57, 317--325. Google ScholarDigital Library
- Tang, C.-S. 1983. Toward a unified logical basis for programming languages. In Proceedings of the 9th World Computer Congress on Information Processing (IFIP'83). 425--429.Google Scholar
- Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its application. Pacific J. Math. 5, 285--309.Google ScholarCross Ref
- Wadge, W. W. 1988. Tense logic programming: A respectable alternative. In Proceedings of the International Symposium on Lucid and Intensional Programming. 26--32.Google Scholar
- Yang, X. and Duan, Z. 2008. Operational semantics of framed tempura. J. Logic Algebraic Program. 78, 1, 22--51.Google ScholarCross Ref
- Yang, X., Duan, Z., and Ma, Q. 2010. Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. 20, 5, 865--914. Google ScholarDigital Library
Index Terms
- Logical foundations for more expressive declarative temporal logic programming languages
Recommendations
A Paraconsistent Linear-time Temporal Logic
Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time ...
Refutation-Aware Gentzen-Style Calculi for Propositional Until-Free Linear-Time Temporal Logic
AbstractThis study introduces refutation-aware Gentzen-style sequent calculi and Kripke-style semantics for propositional until-free linear-time temporal logic. The sequent calculi and semantics are constructed on the basis of the refutation-aware setting ...
Comments