More Web Proxy on the site http://driver.im/

research-article

Logical foundations for more expressive declarative temporal logic programming languages

Authors:

Jose Gaintzarain,

Paqui LucioAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 14, Issue 4

Article No.: 28, Pages 1 - 41

https://doi.org/10.1145/2528931

Published: 28 November 2013 Publication History

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.

References

[1]

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.

[2]

Abadi, M. and Manna, Z. 1989. Temporal logic programming. J. Symbolic Comput. 8, 3, 277--295.

Digital Library

[3]

Aguado, F., Cabalar, P., Perez, G., and Vidal, C. 2008. Strongly equivalent temporal logic programs. In Proceedings of the 11^th European Conference on Logics in Artificial Intelligence (JELIA'08). Lecture Notes in Computer Science, vol. 5293, Springer, 8--20.

Digital Library

[4]

Aguado, F., Cabalar, P., Perez, G., and Vidal, C. 2011. Loop formulas for splitable temporal logic programs. In Proceedings of the 11^th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'11). Lecture Notes in Computer Science, vol. 6645, Springer, 80--92.

Digital Library

[5]

Balbiani, P., Farinas Del Cerro, L., and Herzig, A. 1988. Declarative semantics for modal logic programs. In Proceedings of the International Conference on 5^th Generation Computer Systems (FGCS'88). OHMSHA Ltd. Tokyo and Springer, 507--514.

[6]

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.

Digital Library

[7]

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.

Digital Library

[8]

Baudinet, M. 1989a. Logic programming semantics: Techniques and applications. Ph.D. dissertation. Department of Computer Science, Stanford University, CA.

Digital Library

[9]

Baudinet, M. 1989b. Temporal logic programming is complete and expressive. In Proceedings of the 16^th Annual ACM Symposium on Principles of Programming Languages (POPL'89). ACM Press, New York, 267--280.

Digital Library

[10]

Baudinet, M. 1992. A simple proof of the completeness of temporal logic programming. In Intensional Logics for Programming. Oxford University Press, 51--83.

[11]

Baudinet, M. 1995. On the expressiveness of temporal logic programming. Inf. Comput. 117, 2, 157--180.

Digital Library

[12]

Brunnler, K. and Lange, M. 2008. Cut-free sequent systems for temporal logic. J. Logic Algebraic Program. 76, 2, 216--225.

[13]

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.

[14]

Brzoska, C. 1993. Temporal logic programming with bounded universal modality goals. In Proceedings of the 10^th International Conference on Logic Programming (ICLP'93). MIT Press, 239--256.

Digital Library

[15]

Brzoska, C. 1995a. Temporal logic programming in dense time. In Proceedings of the International Logic Programming Symposium (ILPS'95). MIT Press, 303--317.

[16]

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.

Digital Library

[17]

Brzoska, C. 1998. Programming in metric temporal logic. Theor. Comput. Sci. 202, 1--2, 55--125.

Digital Library

[18]

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.

[19]

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 4^th Euromicro Workshop on Parallel and Distributed Processing (PDP'96). IEEE Computer Society Press, Los Alamitos, CA, 493--500.

Digital Library

[20]

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.

Digital Library

[21]

Clarke, E. M., Grumberg, O., and Peled, D. 2001. Model Checking. MIT Press.

[22]

Dixon, C. and Fisher, M. 1998. The set of support strategy in temporal resolution. In Proceedings of the 5^th International Workshop on Temporal Representation and Reasoning (TIME'98). IEEE Computer Society Press, Los Alamitos, CA, 113--120.

Digital Library

[23]

Dixon, C., Fisher, M., and Konev, B. 2006. Is there a future for deductive temporal verification&quest; In Proceedings of the 13^th International Symposium on Temporal Representation and Reasoning (TIME'06). IEEE Computer Society Press, Los Alamitos, CA, 11--18.

Digital Library

[24]

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.

[25]

Duan, Z., Yang, X., and Koutny, M. 2005. Semantics of framed temporal logic programs. In Proceedings of the 21^st International Conference on Logic Programming (ICLP'05). Lecture Notes in Computer Science, vol. 3668, Springer, 356--370.

Digital Library

[26]

Duan, Z., Yang, X., and Koutny, M. 2008. Framed temporal logic programming. Sci. Comput. Program. 70, 1, 31--61.

Digital Library

[27]

Farinas Del Cerro, L. 1986. MOLOG: A system that extends prolog with modal logic. New Generation Comput. 4, 35--50.

Digital Library

[28]

Fisher, M. 1991. A resolution method for temporal logic. In Proceedings of the 12^th International Joint Conference on Artificial Intelligence (IJCAI'91). Morgan Kaufmann, 99--104.

Digital Library

[29]

Fisher, M. 1992. A normal form for first-order temporal formulae. In Proceedings of the 11^th International Conference on Automated Deduction (CADE'92). Lecture Notes in Computer Science, vol. 607, Springer, 370--384.

Digital Library

[30]

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.

Digital Library

[31]

Fisher, M. 1997. Implementing bdi-like systems by direct execution. In Proceedings of the 15^th International Joint Conference on Artificial Intelligence (IJCAI'97). Morgan Kaufmann, 316--321.

Digital Library

[32]

Fisher, M. 2011. An Introduction to Practical Formal Methods Using Temporal Logic. John Wiley and Sons, Ltd.

Digital Library

[33]

Fisher, M., Dixon, C., and Peim, M. 2001. Clausal temporal resolution. ACM Trans. Comput. Logic 2, 1, 12--56.

Digital Library

[34]

Fisher, M. and Ghidini, C. 2010. Executable specifications of resource-bounded agents. Auton. Agents Multi-Agent Syst. 21, 3, 368--396.

Digital Library

[35]

Fruhwirth, T. W. 1994. Annotated constraint logic programming applied to temporal reasoning. In Proceedings of the 6^th International Symposium on Programming Language Implementation and Logic Programming (PLILP'94). Lecture Notes in Computer Science, vol. 844, Springer, 230--243.

Digital Library

[36]

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.

Digital Library

[37]

Fruhwirth, T. W. 1996. Temporal annotated constraint logic programming. J. Symbolic Comput. 22, 5/6, 555--583.

Digital Library

[38]

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 3^rd International Conference on Logic Programming (ICLP'86). Lecture Notes in Computer Science, vol. 225, Springer, 695--709.

Digital Library

[39]

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.

Digital Library

[40]

Gabbay, D. M. 1987b. Modal and temporal logic programming. In Temporal Logics and Their Application. Academic Press, 197--237.

Digital Library

[41]

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.

[42]

Gaintzarain, J., Hermo, M., Lucio, P., Navarro, M., and Orejas, F. 2013. Invariant-free clausal temporal resolution. J. Autom. Reason. 50, 1, 1--49.

Digital Library

[43]

Gaintzarain, J. and Lucio, P. 2009. A new approach to temporal logic programming. In Proceedings of the 9^th Spanish Conference on Programming and Languages (PROLE'09). 341--350. http://www.sistedes.es/ficheros/actas-conferencias/PROLE/2009.pdf.

[44]

Gergatsoulis, M. 2001. Temporal and modal logic programming languages. In Encyclopedia of Microcomputers, vol. 27, CRC Press, 393--408.

[45]

Gergatsoulis, M., Rondogiannis, P., and Panayiotopoulos, T. 2000. Temporal disjunctive logic programming. New Generation Comput. 19, 1, 87--102.

Digital Library

[46]

Goranko, V., Kyrilov, A., and Shkatov, D. 2010. Tableau tool for testing satisfiability in ltl: Implementation and experimental analysis. In Proceedings of the 6^th Workshop on Methods for Modalities. Electronic Notes in Theoretical Computer Science, vol. 262, Elsevier, 113--125.

Digital Library

[47]

Hrycej, T. 1988. Temporal prolog. In Proceedings of the 8^th European Conference on Artificial Intelligence (ECAI'88). Pitmann Publishing, 296--301.

Digital Library

[48]

Hrycej, T. 1993. A temporal extension of prolog. J. Logic Program. 15, 1--2, 113--145.

Digital Library

[49]

Hustadt, U. and Schmidt, R. A. 1999. An empirical analysis of modal theorem provers. J. Applied Non-Classical Logics 9, 4, 479--522.

[50]

Hustadt, U. and Schmidt, R. A. 2002. Scientific benchmarking with temporal logic decision procedures. In Proceedings of the 8^th International Conference on Principles and Knowledge Representation and Reasoning (KR'02). Morgan Kaufmann, 533--544.

[51]

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.

[52]

Knaster, B. 1928. Un theorem sur les fonctions d'ensembles. Annales de la Societe Polonaise de Mathematique 6, 133--134.

[53]

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.

Digital Library

[54]

Kono, S., Aoyagi, T., Fujita, M., and Tanaka, H. 1985. Implementation of temporal logic programming language tokio. In Proceedings of the 4^th Conference on Logic Programming (LP'85). Lecture Notes in Computer Science, vol. 221, Springer, 138--147.

Digital Library

[55]

Lloyd, J. W. 1984. Foundations of Logic Programming 1^st Ed. Springer.

Digital Library

[56]

Lobo, J., Minker, J., and Rajasekar, A. 1992. Foundations of Disjunctive Logic Programming. MIT Press.

Digital Library

[57]

Merz, S. 1992. Decidability and incompleteness results for first-order temporal logics of linear time. J. Applied Non-Classical Logics 2, 2, 139--156.

[58]

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.

Digital Library

[59]

Moszkowski, B. C. 1986. Executing Temporal Logic Programs. Cambridge University Press.

Digital Library

[60]

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.

Digital Library

[61]

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 8^th Conference on Logic Programming (LP'89). Lecture Notes in Computer Science, vol. 485, Springer, 174--183.

[62]

Nguyen, L. A. 2000. Constructing the least models for positive modal logic programs. Fundamenta Informaticae 42, 1, 29--60.

Digital Library

[63]

Nguyen, L. A. 2003. A fixpoint semantics and an sld-resolution calculus for modal logic programs. Fundamenta Informaticae 55, 1, 63--100.

Digital Library

[64]

Nguyen, L. A. 2006. Multimodal logic programming. Theor. Comput. Sci. 360, 1--3, 247--288.

Digital Library

[65]

Nguyen, L. A. 2009. Modal logic programming revisited. J. Applied Non-Classical Logics 19, 2, 167--181.

[66]

Orgun, M. A. 1991. Intensional logic programming. Ph.D. dissertation. Department of Computer Science, University of Victoria, British Columbia, Canada.

Digital Library

[67]

Orgun, M. A. 1994. Temporal and modal logic programming: An annotated bibliography. SIGART Bull. 5, 3, 52--59.

Digital Library

[68]

Orgun, M. A. 1995. Foundations of linear-time logic programming. Int. J. Comput. Math. 58, 3--4, 199--219.

[69]

Orgun, M. A. and Ma, W. 1994. An overview of temporal and modal logic programming. In Proceedings of the 1^st International Conference on Temporal Logic (ICTL'94). Lecture Notes in Computer Science, vol. 827, Springer, 445--479.

Digital Library

[70]

Orgun, M. A. and Wadge, W. W. 1992. Towards a unified theory of intensional logic programming. J. Logic Program. 13, 4, 413--440.

Digital Library

[71]

Orgun, M. A. and Wadge, W. W. 1994. Extending temporal logic programming with choice predicates non-determinism. J. Logic Comput. 4, 6, 877--903.

[72]

Orgun, M. A., Wadge, W. W., and Du, W. 1993. Chronolog (Z): Linear-time logic programming. In Proceedings of the 5^th International Conference on Computing and Information (ICCI'93). IEEE Computer Society Press, Los Alamitos, CA, 545--549.

Digital Library

[73]

Paech, B. 1988. Gentzen-systems for propositional temporal logics. In Proceedings of the 2^nd Workshop on Computer Science Logic (CSL'88). Lecture Notes in Computer Science, vol. 385, Springer, 240--253.

Digital Library

[74]

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.

Digital Library

[75]

Pliuskevicius, R. 1992. Logical foundation for logic programming based on first order linear temporal logic. In Proceedings of the 1^st and 2^nd Russian Conference on Logic Programming (RCLP'92). Lecture Notes in Computer Science, vol. 592, Springer, 391--406.

Digital Library

[76]

Raffaeta, A. and Fruhwirth, T. W. 1999. Two semantics for temporal annotated constraint logic programming. In Proceedings of the 12^th International Symposium on Languages for Intensional Programming (ISLIP'99). World Scientific Press, 126--140.

[77]

Reichgelt, H. 1987. Semantics for reified temporal logic. In Advances in Artificial Intelligence. John Wiley and Sons, Ltd., 49--61.

Digital Library

[78]

Rondogiannis, P., Gergatsoulis, M., and Panayiotopoulos, T. 1997. Cactus: A branching-time logic programming language. In Proceedings of the 1^st International Joint Conference on Qualitative and Quantitative Practical Reasoning (ECSQARU-FAPR'97). Lecture Notes in Computer Science, vol. 1244, Springer, 511--524.

Digital Library

[79]

Rondogiannis, P., Gergatsoulis, M., and Panayiotopoulos, T. 1998. Branching-time logic programming: The language cactus and its applications. Comput. Lang. 24, 3, 155--178.

Digital Library

[80]

Sakuragawa, T. 1986. Temporal prolog. Tech. rep. Kyoto University. http://repository.kulib.kyoto-u.ac.jp/dspace/bitstream/2433/99379/1/0586-16.pdf.

[81]

Schoning, U. 1989. Logic for Computer Scientists. Birkhauser.

Digital Library

[82]

Shoham, Y. 1986. Reified temporal logics: Semantical and ontological considerations. In Proceedings of the 7^th European Conference on Artificial Intelligence (ECAI'86). 183--190.

[83]

Sistla, A. P. and Clarke, E. M. 1985. The complexity of propositional linear temporal logics. J. ACM 32, 3, 733--749.

Digital Library

[84]

Szalas, A. 1995. Temporal logic of programs: A standard approach. In Time and Logic. A Computational Approach, UCL Press Ltd., 1--50.

Digital Library

[85]

Szalas, A. and Holenderski, L. 1988. Incompleteness of first-order temporal logic with until. Theor. Comput. Sci. 57, 317--325.

Digital Library

[86]

Tang, C.-S. 1983. Toward a unified logical basis for programming languages. In Proceedings of the 9^th World Computer Congress on Information Processing (IFIP'83). 425--429.

[87]

Tarski, A. 1955. A lattice-theoretical fixpoint theorem and its application. Pacific J. Math. 5, 285--309.

[88]

Wadge, W. W. 1988. Tense logic programming: A respectable alternative. In Proceedings of the International Symposium on Lucid and Intensional Programming. 26--32.

[89]

Yang, X. and Duan, Z. 2008. Operational semantics of framed tempura. J. Logic Algebraic Program. 78, 1, 22--51.

[90]

Yang, X., Duan, Z., and Ma, Q. 2010. Axiomatic semantics of projection temporal logic programs. Math. Struct. Comput. Sci. 20, 5, 865--914.

Digital Library

Cited By

Hu FLiao RChen J(2023)Calculation Methods to Optimize the Number of Pedestals and Evaluate Production Plans for Precast Yards Fabricating Prestressed Bridge Beams and Precast Segments for Poststressed Segmental ErectionJournal of Construction Engineering and Management10.1061/(ASCE)CO.1943-7862.0002404149:1Online publication date: Jan-2023
https://doi.org/10.1061/(ASCE)CO.1943-7862.0002404
Triska JVychodil V(2017)Logic of temporal attribute implicationsAnnals of Mathematics and Artificial Intelligence10.1007/s10472-016-9526-679:4(307-335)Online publication date: 1-Apr-2017
https://dl.acm.org/doi/10.1007/s10472-016-9526-6
Negreanu L(2015)Declarative Programming with Temporal Constraints, in the Language CGThe Scientific World Journal10.1155/2015/5408542015:1Online publication date: 29-Mar-2015
https://doi.org/10.1155/2015/540854

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
Abstract
This 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 ...
Declarative foundations of higher-order logic programming

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 14, Issue 4

November 2013

282 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/2555591

Issue’s Table of Contents

Copyright © 2013 ACM.

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: 28 November 2013

Accepted: 01 February 2013

Received: 01 November 2012

Published in TOCL Volume 14, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Spanish Project TIN2007-66523
Euskal Herriko Unibertsitatea

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
199
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hu FLiao RChen J(2023)Calculation Methods to Optimize the Number of Pedestals and Evaluate Production Plans for Precast Yards Fabricating Prestressed Bridge Beams and Precast Segments for Poststressed Segmental ErectionJournal of Construction Engineering and Management10.1061/(ASCE)CO.1943-7862.0002404149:1Online publication date: Jan-2023
https://doi.org/10.1061/(ASCE)CO.1943-7862.0002404
Triska JVychodil V(2017)Logic of temporal attribute implicationsAnnals of Mathematics and Artificial Intelligence10.1007/s10472-016-9526-679:4(307-335)Online publication date: 1-Apr-2017
https://dl.acm.org/doi/10.1007/s10472-016-9526-6
Negreanu L(2015)Declarative Programming with Temporal Constraints, in the Language CGThe Scientific World Journal10.1155/2015/5408542015:1Online publication date: 29-Mar-2015
https://doi.org/10.1155/2015/540854

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents