{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T17:30:40Z","timestamp":1778520640194,"version":"3.51.4"},"reference-count":112,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T00:00:00Z","timestamp":1640563200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Theory and Practice of Logic Programming"],"published-print":{"date-parts":[[2023,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this survey, we present an overview on (Modal) Temporal Logic Programming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in <jats:italic>Linear-time Temporal Logic<\/jats:italic> (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called <jats:italic>Temporal Equilibrium Logic<\/jats:italic> (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on <jats:italic>Equilibrium Logic<\/jats:italic>, a well known logical characterization of Answer Set Programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium Logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called <jats:italic>(modal) temporal logic programs<\/jats:italic> closer to ASP, and explaining how this has been exploited in the construction of the solver <jats:monospace>telingo<\/jats:monospace>, a temporal extension of the well-known ASP solver <jats:monospace>clingo<\/jats:monospace> that uses its incremental solving capabilities.<\/jats:p>","DOI":"10.1017\/s1471068421000557","type":"journal-article","created":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T07:07:31Z","timestamp":1640588851000},"page":"2-56","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":15,"title":["Linear-Time Temporal Answer Set Programming"],"prefix":"10.1017","volume":"23","author":[{"given":"FELICIDAD","family":"AGUADO","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7440-0953","authenticated-orcid":false,"given":"PEDRO","family":"CABALAR","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3440-4348","authenticated-orcid":false,"given":"MART\u00cdN","family":"DI\u00c9GUEZ","sequence":"additional","affiliation":[]},{"given":"GILBERTO","family":"P\u00c9REZ","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7456-041X","authenticated-orcid":false,"given":"TORSTEN","family":"SCHAUB","sequence":"additional","affiliation":[]},{"given":"ANNA","family":"SCHUHMANN","sequence":"additional","affiliation":[]},{"given":"CONCEPCI\u00d3N","family":"VIDAL","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2021,12,27]]},"reference":[{"key":"S1471068421000557_ref72","first-page":"65","article-title":"Zum intuitionistischen Aussagenkalk\u00fcl","author":"G\u00f6del","year":"1932","journal-title":"Anzeiger der Akademie der Wissenschaften in Wien"},{"key":"S1471068421000557_ref31","unstructured":"Cabalar, P. 1999. Temporal answer sets. In Proceedings of the Joint Conference on Declarative Programming (AGP\u201999), Meo, M. and Ferro, M. , Eds, 351\u2013366."},{"key":"S1471068421000557_ref37","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000307"},{"key":"S1471068421000557_ref62","doi-asserted-by":"crossref","unstructured":"Gabbay, D. 1987a. The declarative past and imperative future: Executable temporal logic for interactive systems. In Proceedings of the Conference on Temporal Logic in Specification, Banieqbal, B. , Barringer, H. and Pnueli, A. , Eds. Lecture Notes in Computer Science, vol. 398. Springer-Verlag, 409\u2013448.","DOI":"10.1007\/3-540-51803-7_36"},{"key":"S1471068421000557_ref85","unstructured":"Lee, J. , Lifschitz, V. and Yang, F. 2013. Action language BC: Preliminary report. In Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI\u201913), F. Rossi, Ed. IJCAI\/AAAI Press, 983\u2013989."},{"key":"S1471068421000557_ref76","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"S1471068421000557_ref24","unstructured":"Bosser, A. , Cabalar, P. , Di\u00e9guez, M. and Schaub, T. 2018. Introducing temporal stable models for linear dynamic logic. In Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201918), Thielscher, M. , Toni, F. , and Wolter, F. , Eds. AAAI Press, 12\u201321."},{"key":"S1471068421000557_ref111","doi-asserted-by":"crossref","unstructured":"Zhu, S. , Pu, G. and Vardi, M. 2019. First-order vs. second-order encodings for LTLf-to-automata translation. In Proceedings of the Fifteenth Annual Conference on Theory and Applications of Models of Computation (TAMC\u201919), Gopal, T. and Watada, J. , Eds. Lecture Notes in Computer Science, vol. 11436. Springer-Verlag, 684\u2013705.","DOI":"10.1007\/978-3-030-14812-6_43"},{"key":"S1471068421000557_ref22","doi-asserted-by":"crossref","unstructured":"Bieber, P. , Fari\u00f1as del Cerro, L. and Herzig, A. 1988. MOLOG: a modal PROLOG. In Proceedings of the Nineth International Conference on Automated Deduction (CADE\u201988), Lusk, E. and Overbeek, R. , Eds. Lecture Notes in Computer Science, vol. 310. Springer-Verlag, 762\u2013763.","DOI":"10.1007\/BFb0012886"},{"key":"S1471068421000557_ref32","doi-asserted-by":"crossref","unstructured":"Cabalar, P. and Demri, S. 2011. Automata-based computation of temporal equilibrium models. In Proceedings of the Twenty-first International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR\u201911), G. Vidal, Ed. Notes, Lecture in Computer Science, vol. 7225. Springer-Verlag, 57\u201372.","DOI":"10.1007\/978-3-642-32211-2_5"},{"key":"S1471068421000557_ref78","doi-asserted-by":"crossref","unstructured":"Henriksen, J. , Jensen, J. , J\u00f8rgensen, M. , Klarlund, N. , Paige, R. , Rauhe, T. and Sandholm, A. 1995. Mona: Monadic second-order logic in practice. In Proceedings of the First International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201995), Brinksma, E. , Cleaveland, R. , Larsen, K. , Margaria, T. and Steffen, B. , Eds. Lecture Notes in Computer Science, vol. 1019. Springer-Verlag, 89\u2013110.","DOI":"10.1007\/3-540-60630-0_5"},{"key":"S1471068421000557_ref97","doi-asserted-by":"crossref","unstructured":"Pearce, D. , Tompits, H. and Woltran, S. 2001. Encodings for equilibrium logic and logic programs with nested expressions. In Proceedings of the Tenth Portuguese Conference on Artificial Intelligence (EPIA\u201901), Brazdil, P. and Jorge, A. , Eds. Lecture Notes in Computer Science, vol. 2258. Springer-Verlag, 306\u2013320.","DOI":"10.1007\/3-540-45329-6_31"},{"key":"S1471068421000557_ref41","doi-asserted-by":"crossref","unstructured":"Cabalar, P. and Schaub, T. 2019. Temporal logic programs with temporal description logic axioms. In Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, Lutz, C. , Sattler, U. , Tinelli, C. , Turhan, A. and Wolter, F. , Eds. Lecture Notes in Computer Science, vol. 11560. Springer-Verlag, 174\u2013186.","DOI":"10.1007\/978-3-030-22102-7_8"},{"key":"S1471068421000557_ref94","unstructured":"Oikarinen, E. and Janhunen, T. 2006. Modular equivalence for normal logic programs. In Proceedings of the Seventeenth European Conference on Artificial Intelligence (ECAI\u201906), Brewka, G. , Coradeschi, S. , Perini, A. and Traverso, P. , Eds. IOS Press, 412\u2013416."},{"key":"S1471068421000557_ref110","doi-asserted-by":"crossref","unstructured":"Wolper, P. 1983. Temporal logic can be more expressive. Information and Control 56, 1\/2, 72\u201399.","DOI":"10.1016\/S0019-9958(83)80051-5"},{"key":"S1471068421000557_ref34","unstructured":"Cabalar, P. and Di\u00e9guez, M. 2014. Strong equivalence of non-monotonic temporal theories. In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201914), Baral, C. , De Giacomo, G. and Eiter, T. , Eds. AAAI Press."},{"key":"S1471068421000557_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/151634.151635"},{"key":"S1471068421000557_ref104","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"S1471068421000557_ref30","unstructured":"B\u00fcchi, J. 1962. On a decision method in restricted second order arithmetic. In Proceedings of the International Congress on Logic, Methodology, and Philosophy of Science, Nagel, E. , Suppes, P. , and Tarski, A. , Eds. Stanford University Press, 1\u201311."},{"key":"S1471068421000557_ref86","doi-asserted-by":"publisher","DOI":"10.1016\/S0743-1066(96)00121-5"},{"key":"S1471068421000557_ref71","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/9.2.273"},{"key":"S1471068421000557_ref109","doi-asserted-by":"crossref","unstructured":"Wa\u0142ega, P. , Tena Cucala, D. , Kostylev, E. and Cuenca Grau, B. 2020. DatalogMTL with negation under stable models semantics. In Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201922), Bienvenu, M. , Lakemeyer, G. , and Erdem, E. , Eds. AAAI Press, 609\u2013618.","DOI":"10.24963\/kr.2021\/58"},{"key":"S1471068421000557_ref38","doi-asserted-by":"crossref","unstructured":"Cabalar, P. , Kaminski, R. , Morkisch, P. and Schaub, T. 2019. telingo = ASP + time. In Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201919), Balduccini, M. , Lierler, Y. , and Woltran, S. , Eds. Lecture Notes in Artificial Intelligence, vol. 11481. Springer-Verlag, 256\u2013269.","DOI":"10.1007\/978-3-030-20528-7_19"},{"key":"S1471068421000557_ref8","first-page":"832","article-title":"Maintaining knowledge about temporal intervals","volume":"11","year":"1983","journal-title":"Communications of the ACM 26"},{"key":"S1471068421000557_ref19","unstructured":"Beck, H. , Dao-Tran, M. and Eiter, T. 2016. Equivalent stream reasoning programs. In Proceedings of the Twenty-fifth International Joint Conference on Artificial Intelligence (IJCAI\u201916), R. Kambhampati, Ed. IJCAI\/AAAI Press, 929\u2013935."},{"key":"S1471068421000557_ref7","doi-asserted-by":"crossref","unstructured":"Aguado, F. , P\u00e9rez, G. and Vidal, C. 2013. Integrating temporal extensions of answer set programming. In Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201913), Cabalar, P. and Son, T. , Eds. Lecture Notes in Artificial Intelligence, vol. 8148. Springer-Verlag, 23\u201335.","DOI":"10.1007\/978-3-642-40564-8_3"},{"key":"S1471068421000557_ref75","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00447-4"},{"key":"S1471068421000557_ref79","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00039-6"},{"key":"S1471068421000557_ref89","first-page":"82","article-title":"Die logik und das grundlagenproblem","volume":"6\u20139","author":"Lukasiewicz","year":"1941","journal-title":"Les Entreties de Z\u00fcrich sur les Fondaments et la M\u00e9thode des Sciences Math\u00e9matiques 12"},{"key":"S1471068421000557_ref100","doi-asserted-by":"crossref","unstructured":"Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the Eight-teenth Symposium on Foundations of Computer Science (FOCS\u201977). IEEE Computer Society Press, 46\u201357.","DOI":"10.1109\/SFCS.1977.32"},{"key":"S1471068421000557_ref15","doi-asserted-by":"crossref","unstructured":"Balbiani, P. and Di\u00e9guez, M. 2016. Temporal here and there. In Proceedings of the Fifteenth European Conference on Logics in Artificial Intelligence (JELIA\u201916), Michael, L. and Kakas, A. , Eds. Lecture Notes in Artificial Intelligence, vol. 10021. Springer-Verlag, 81\u201396.","DOI":"10.1007\/978-3-319-48758-8_6"},{"key":"S1471068421000557_ref57","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"S1471068421000557_ref105","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90008-9"},{"key":"S1471068421000557_ref21","unstructured":"Bertoli, P. , Cimatti, A. , Roveri, M. and Traverso, P. 2001. Planning in nondeterministic domains under partial observability via symbolic model checking. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI\u201901), B. Nebel, Ed. Morgan Kaufmann Publishers, 473\u2013478."},{"key":"S1471068421000557_ref93","volume-title":"Executing Temporal Logic Programs","author":"Moszkowski","year":"1986"},{"key":"S1471068421000557_ref17","unstructured":"Baudinet, M. 1992. A simple proof of the completeness of temporal logic programming. In Fari\u00f1as del Cerro, L. and Penttonen, M. , Eds. Clarendon Press, 51\u201383."},{"key":"S1471068421000557_ref67","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90035-F"},{"key":"S1471068421000557_ref9","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016636131405"},{"key":"S1471068421000557_ref82","unstructured":"Hrycej, T. 1988. Temporal Prolog. In Proceedings of the Eighth European Conference on Artificial Intelligence (ECAI\u201992), Y. Kodratoff, Ed. Pitman\/Morgan Kaufmann, 296\u2013301."},{"key":"S1471068421000557_ref103","unstructured":"Sistla, A. 1983. Theoretical issues in the design and verification of distributed systems. Ph.D. thesis, Harvard University."},{"key":"S1471068421000557_ref3","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2018.1427987"},{"key":"S1471068421000557_ref46","doi-asserted-by":"crossref","unstructured":"Chomicki, J. and Imielinski, T. 1988. Temporal deductive databases and infinite objects. In Proceedings of the Seventh ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, Edmondson-Yurkanan, C. and Yannakakis, M. , Eds. ACM Press, 61\u201373.","DOI":"10.1145\/308386.308416"},{"key":"S1471068421000557_ref42","doi-asserted-by":"crossref","unstructured":"Cabalar, P. and Vega, G. P. 2007. Temporal equilibrium logic: A first approach. In Proceedings of the Eleventh International Conference on Computer Aided Systems Theory (EUROCAST\u201917), Moreno-Daz, R. , Pichler, F. and Quesada-Arencibia, A. , Eds. Lecture Notes in Computer Science, vol. 4739. Springer-Verlag, 241\u2013248.","DOI":"10.1007\/978-3-540-75867-9_31"},{"key":"S1471068421000557_ref99","unstructured":"Pistore, M. and Traverso, P. 2001. Planning as model checking for extended goals in non-deterministic domains. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI\u201901), B. Nebel, Ed. Morgan Kaufmann Publishers, 479\u2013486."},{"key":"S1471068421000557_ref107","doi-asserted-by":"publisher","DOI":"10.1145\/321978.321991"},{"key":"S1471068421000557_ref20","unstructured":"Beck, H. , Dao-Tran, M. , Eiter, T. and Fink, M. 2015. LARS: A logic-based framework for analyzing reasoning over streams. In Proceedings of the Twenty-Ninth National Conference on Artificial Intelligence (AAAI\u201915), Bonet, B. and Koenig, S. , Eds. AAAI Press, 1431\u20131438."},{"key":"S1471068421000557_ref69","unstructured":"Giordano, L. , Martelli, A. and Dupr\u00e9, D. T. 2012. Achieving completeness in bounded model checking of action theories in ASP. In Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (KR\u201912), Brewka, G. , Eiter, T. and McIlraith, S. , Eds. AAAI Press."},{"key":"S1471068421000557_ref53","unstructured":"Eiter, T. and \u0160imkus, M. 2009. Bidirectional answer set programs with function symbols. In Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI\u201909), C. Boutilier, Ed. AAAI\/MIT Press, 765\u2013771."},{"key":"S1471068421000557_ref59","unstructured":"French, T. and Reynolds, M. 2002. A sound and complete proof system for QPTL. In Proceedings of the Fourth Conference on Advances in Modal Logic, Balbiani, P. , Suzuki, N. , Wolter, F. , and Zakharyaschev, M. , Eds. King\u2019s College Publications, 127\u2013148."},{"key":"S1471068421000557_ref87","doi-asserted-by":"crossref","unstructured":"Li, J. 2012. Qualitative spatial and temporal reasoning with answer set programming. In Proceedings of the Twenty-fourth IEEE International Conference on Tools with Artificial Intelligence (ICTAI\u201912). IEEE Computer Society Press, 603\u2013609.","DOI":"10.1109\/ICTAI.2012.87"},{"key":"S1471068421000557_ref95","unstructured":"Orgun, M. and Wadge, W. 1990. Theory and practice of temporal logic programming. Fari\u00f1as del Cerro, L. and Penttonen, M. , Eds. Clarendon Press, 21\u201350."},{"key":"S1471068421000557_ref77","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068403001790"},{"key":"S1471068421000557_ref70","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068411000639"},{"key":"S1471068421000557_ref108","doi-asserted-by":"crossref","unstructured":"Wa\u0142ega, P. , Cuenca Grau, B. , Kaminski, M. and Kostylev, E. 2019. DatalogMTL: Computational complexity and expressive power. In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence (IJCAI\u201919), S. Kraus, Ed. ijcai.org, 1886\u20131892.","DOI":"10.24963\/ijcai.2019\/261"},{"key":"S1471068421000557_ref10","doi-asserted-by":"crossref","unstructured":"Artale, A. and Franconi, E. 2005. Temporal description logics. In Handbook of Temporal Reasoning in Artificial Intelligence, Fisher, M. , Gabbay, D. and Vila, L. , Eds. Foundations of Artificial Intelligence, vol. 1. Elsevier Science, 375\u2013388.","DOI":"10.1016\/S1574-6526(05)80014-8"},{"key":"S1471068421000557_ref39","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068418000297"},{"key":"S1471068421000557_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/s10115-010-0294-z"},{"key":"S1471068421000557_ref65","doi-asserted-by":"crossref","unstructured":"Gebser, M. , Kaminski, R. , Kaufmann, B. and Schaub, T. 2019. Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming 19, 1, 27\u201382.","DOI":"10.1017\/S1471068418000054"},{"key":"S1471068421000557_ref88","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(02)00186-8"},{"key":"S1471068421000557_ref29","unstructured":"Brzoska, C. 1995. Temporal logic programming in dense time. In Proceedings of the International Symposium on Logic Programming, J. Lloyd, Ed. Press, MIT , 303\u2013317."},{"key":"S1471068421000557_ref16","doi-asserted-by":"crossref","unstructured":"Baldoni, M. , Giordano, L. , Martelli, A. and Patti, V. 1997. An abductive proof procedure for reasoning about actions in modal logic programming. In Proceedings of the Sixth International Workshop on Non-Monotonic Extensions of Logic Programming (NMELP\u201996), Dix, J. , Pereira, L. , and Przymusinski, T. , Eds. Lecture Notes in Computer Science, vol. 1216. Springer-Verlag, 132\u2013150.","DOI":"10.1007\/BFb0023805"},{"key":"S1471068421000557_ref50","unstructured":"De Giacomo, G. and Vardi, M. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI\u201913), F. Rossi, Ed. IJCAI\/AAAI Press, 854\u2013860."},{"key":"S1471068421000557_ref81","first-page":"183","article-title":"The axiomatization of the intermediate propositional systems \n\n\n\n$s_2$\n\n\n of G\u00f6del","volume":"2","author":"Hosoi","year":"1966","journal-title":"Journal of the Faculty of Science of the University of Tokyo 13"},{"key":"S1471068421000557_ref33","doi-asserted-by":"crossref","unstructured":"Cabalar, P. and Di\u00e9guez, M. 2011. STELP \u2014 A tool for temporal answer set programming. In Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR\u201911), Delgrande, J. and Faber, W. , Eds. Lecture Notes in Artificial Intelligence, vol. 6645. Springer-Verlag, 370\u2013375.","DOI":"10.1007\/978-3-642-20895-9_43"},{"key":"S1471068421000557_ref84","unstructured":"Kvarnstr\u00f6m, J. , Heintz, F. and Doherty, P. 2008. A temporal logic-based planning and execution monitoring system. In Proceedings of the Eighteenth International Conference on Automated Planning and Scheduling (ICAPS\u201908), Rintanen, J. , Nebel, B. , Beck, J. and Hansen, E. , Eds. AAAI Press, 198\u2013205."},{"key":"S1471068421000557_ref74","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504079"},{"key":"S1471068421000557_ref83","unstructured":"Kamp, J. 1968. Tense logic and the theory of linear order. Ph.D. thesis, University of California at Los Angeles."},{"key":"S1471068421000557_ref49","unstructured":"De Giacomo, G. and Perelli, G. 2021. Behavioral QLTL. CoRR abs\/2102.11184."},{"key":"S1471068421000557_ref12","unstructured":"Baader, F. , Ghilardi, S. and Lutz, C. 2008. LTL over description logic axioms. In Proceedings of the Eleventh International Conference on Principles of Knowledge Representation and Reasoning (KR\u201908), Brewka, G. and Lang, J. , Eds. AAAI Press, 684\u2013694."},{"key":"S1471068421000557_ref101","unstructured":"Schwind, C. 1997. A logic based framework for action theories. In Proceedings of the Tbilisi Symposium on Logic, Language and Computation, Ginzburg, J. , Khasidashvili, Z. , Vogel, C. , L\u00e9vy, J. and Vallduv\u00ed, E. , Eds. 275\u2013291."},{"key":"S1471068421000557_ref80","unstructured":"Heyting, A. 1930. Die formalen Regeln der intuitionistischen Logik. In Sitzungsberichte der Preussischen Akademie der Wissenschaften. Deutsche Akademie der Wissenschaften zu Berlin, 42\u201356."},{"key":"S1471068421000557_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"S1471068421000557_ref54","first-page":"51","article-title":"Consistency of Clark\u2019s completion and the existence of stable models","author":"Fages","year":"1994","journal-title":"Journal of Methods of Logic in Computer Science 1"},{"key":"S1471068421000557_ref91","unstructured":"Mendez, G. , Llopis, J. , Lobo, J. and Baral, C. 1996. Temporal logic and reasoning about actions. In Proceedings of the Third Symposium on Logical Formalizations of Commonsense Reasoning."},{"key":"S1471068421000557_ref52","doi-asserted-by":"crossref","unstructured":"Duret-Lutz, A. , Lewkowicz, A. , Fauchille, A. , Michaud, T. , Renault, E. and Xu, L. 2016. Spot 2.0 \u2013 A framework for LTL and $\\omega$ -automata manipulation. In Proceedings of Fourteenth International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916), Artho, C. , Legay, A. and Peled, D. , Eds. Lecture Notes in Computer Science, vol. 9938. 122\u2013129.","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"S1471068421000557_ref56","unstructured":"Ferraris, P. , Lee, J. and Lifschitz, V. 2007. A new perspective on stable models. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI\u201907), M. Veloso, Ed. AAAI\/MIT Press, 372\u2013379."},{"key":"S1471068421000557_ref1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80070-7"},{"key":"S1471068421000557_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00071-5"},{"key":"S1471068421000557_ref90","doi-asserted-by":"crossref","unstructured":"Lutz, C. , Wolter, F. and Zakharyaschev, M. 2008. Temporal description logics: A survey. In Proceedings of the fifteenth International Symposium on Temporal Representation and Reasoning (TIME\u201908), Demri, S. and Jensen, C. , Eds. IEEE Computer Society Press, 3\u201314.","DOI":"10.1109\/TIME.2008.14"},{"key":"S1471068421000557_ref27","unstructured":"Brenton, C. , Faber, W. and Batsakis, S. 2016. Answer set programming for qualitative spatio-temporal reasoning: Methods and experiments. In Technical Communications of the Thirty-second International Conference on Logic Programming (ICLP\u201916), Carro, M. and King, A. , Eds. OpenAccess Series in Informatics (OASIcs), vol. 52. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, 4:1\u20134:15."},{"key":"S1471068421000557_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068416000570"},{"key":"S1471068421000557_ref61","doi-asserted-by":"crossref","unstructured":"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 Third International Conference on Logic Programming (ICLP\u201986), E. Shapiro, Ed. Notes, Lecture in Computer Science, vol. 225. Springer, 695\u2013709.","DOI":"10.1007\/3-540-16492-8_119"},{"key":"S1471068421000557_ref106","doi-asserted-by":"crossref","unstructured":"van Dalen, D. 2001. Intuitionistic logic. In Handbook of Philosophical Logic, Gabbay, D. and Guenthner, F. , Eds. Vol. 3. Springer-Verlag, 225\u2013339.","DOI":"10.1007\/978-94-009-5203-4_4"},{"key":"S1471068421000557_ref23","doi-asserted-by":"crossref","unstructured":"Biere, A. , Cimatti, A. , Clarke, E. and Zhu, Y. 1999. Symbolic model checking without BDDs. In Proceedings of the Fifth International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u201999), R. Cleaveland, Ed. Notes, Lecture in Computer Science, vol. 1579. Springer-Verlag, 193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"S1471068421000557_ref4","unstructured":"Aguado, F. , Cabalar, P. , Fandinno, J. , P\u00e9rez, G. and Vidal, C. 2020. Explicit negation in linear-dynamic equilibrium logic. In Proceedings of the Twenty-fourth European Conference on Artificial Intelligence (ECAI\u201920), De Giacomo, G. , Catal\u00e1, A. , Dilkina, B. , Milano, M. , Barro, S. , Bugarn, A. and Lang, J. , Eds. IOS Press, 569\u2013576."},{"key":"S1471068421000557_ref36","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068420000307"},{"key":"S1471068421000557_ref44","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/9.5.701"},{"key":"S1471068421000557_ref98","doi-asserted-by":"crossref","unstructured":"Pearce, D. and Valverde, A. 2008. Quantified equilibrium logic and foundations for answer set programs. In Proceedings of the Twenty Fourth International Conference of Logic Programming (ICLP\u201908), Garcia De La Banda, M. and Pontelli, E. , Eds. Lecture Notes in Computer Science, vol. 5366. Springer-Verlag, 546\u2013560.","DOI":"10.1007\/978-3-540-89982-2_46"},{"key":"S1471068421000557_ref68","doi-asserted-by":"crossref","unstructured":"Gerth, R. , Peled, D. , Vardi, M. and Wolper, P. 1995. Simple on-the-fly automatic verification of linear temporal logic. In Proceedings of the Fifteenth IFIP International Symposium on Protocol Specification, Dembinski, P. and Sredniawa, M. , Eds. IFIP Conference Proceedings, vol. 38. Chapman & Hall, 3\u201318.","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"S1471068421000557_ref26","doi-asserted-by":"crossref","unstructured":"Bozzelli, L. and Pearce, D. 2015. On the complexity of temporal equilibrium logic. In Proceedings of the Thirtieth Annual Symposium on Logic in Computer Science (LICS\u201915). IEEE Computer Society Press, 645\u2013656.","DOI":"10.1109\/LICS.2015.65"},{"key":"S1471068421000557_ref64","doi-asserted-by":"crossref","unstructured":"Gabbay, D. , Pnueli, A. , Shelah, S. and Stavi, J. 1980. On the temporal basis of fairness. In Proceedings of the Seventh Symposium on Principles of Programming Languages (POPL\u201980), Abrahams, P. , Lipton, R. and Bourne, S. , Eds. ACM Press, 163\u2013173.","DOI":"10.1145\/567446.567462"},{"key":"S1471068421000557_ref43","doi-asserted-by":"crossref","unstructured":"Camacho, A. , Baier, J. , Muise, C. and McIlraith, S. 2018. Finite LTL synthesis as planning. In Proceedings of the Twenty-Eighth International Conference on Automated Planning and Scheduling (ICAPS\u201918), de Weerdt, M. , Koenig, S. , R\u00f6ger, G. and Spaan, M. , Eds. AAAI Press, 29\u201338.","DOI":"10.24963\/ijcai.2018\/848"},{"key":"S1471068421000557_ref73","unstructured":"Goldblatt, R. 1992. Logics of Time and Computation. Number 7 in CSLI Lecture Notes. Center for the Study of Language and Information."},{"key":"S1471068421000557_ref11","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","author":"Baader","year":"2003"},{"key":"S1471068421000557_ref40","doi-asserted-by":"crossref","unstructured":"Cabalar, P. , Rey, M. and Vidal, C. 2019. A complete planner for temporal answer set programming. In Proceedings of the Nineteenth EPIA Conference on Artificial Intelligence, (EPIA\u201919), Oliveira, P. , Novais, P. , and Reis, L. , Eds. Lecture Notes in Computer Science, vol. 11805. Springer, 520\u2013525.","DOI":"10.1007\/978-3-030-30244-3_43"},{"key":"S1471068421000557_ref58","doi-asserted-by":"crossref","unstructured":"Fisher, M. 1994. A survey of concurrent METATEM \u2013 The language and its applications. In Proceedings of the First International Conference on Temporal Logic (ICTL\u201994), Gabbay, D. and Ohlbach, H. , Eds. Lecture Notes in Computer Science, vol. 827. Springer-Verlag, 480\u2013505.","DOI":"10.1007\/BFb0014005"},{"key":"S1471068421000557_ref51","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"Demri","year":"2016"},{"key":"S1471068421000557_ref66","unstructured":"Gelfond, M. and Lifschitz, V. 1988. Compiling circumscriptive theories into logic programs. In Proceedings of the Seventh National Conference on Artificial Intelligence (AAAI\u201988), Shrobe, H. , Mitchell, T. and Smith, R. , Eds. AAAI Press\/The MIT Press, 455\u2013459."},{"key":"S1471068421000557_ref96","doi-asserted-by":"crossref","unstructured":"Pearce, D. 1997. A new logical characterisation of stable models and answer sets. In Proceedings of the Sixth International Workshop on Non-Monotonic Extensions of Logic Programming (NMELP\u201996), Dix, J. , Pereira, L. and Przymusinski, T. , Eds. Lecture Notes in Computer Science, vol. 1216. Springer-Verlag, 57\u201370.","DOI":"10.1007\/BFb0023801"},{"key":"S1471068421000557_ref112","doi-asserted-by":"crossref","unstructured":"Zhu, S. , Tabajara, L. , Li, J. , Pu, G. and Vardi, M. 2017. Symbolic LTLf synthesis. In Proceedings of the Twenty-sixth International Joint Conference on Artificial Intelligence (IJCAI\u201917), C. Sierra, Ed. IJCAI\/AAAI Press, 1362\u20131369.","DOI":"10.24963\/ijcai.2017\/189"},{"key":"S1471068421000557_ref28","unstructured":"Brzoska, C. 1991. Temporal logic programming and its relation to constraint logic programming. In Proceedings of the International Symposium on Logic Programming, Saraswat, V. and Ueda, K. , Eds. MIT Press, 661\u2013677."},{"key":"S1471068421000557_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068415000277"},{"key":"S1471068421000557_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/BF03037381"},{"key":"S1471068421000557_ref35","unstructured":"Cabalar, P. , Di\u00e9guez, M. , Laferriere, F. and Schaub, T. 2020. Implementing dynamic answer set programming over finite traces. In Proceedings of the Twenty-fourth European Conference on Artificial Intelligence (ECAI\u201920), De Giacomo, G. , Catal\u00e1, A. , Dilkina, B. , Milano, M. , Barro, S. , Bugarn, A. and Lang, J. , Eds. IOS Press, 656\u2013663."},{"key":"S1471068421000557_ref63","unstructured":"Gabbay, D. 1987b. Modal and temporal logic programming. In Temporal Logics and their Applications, A. Galton, Ed. Press, Academic , Chapter 6, 197\u2013237."},{"key":"S1471068421000557_ref102","unstructured":"Simpson, A. 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh."},{"key":"S1471068421000557_ref92","doi-asserted-by":"crossref","unstructured":"Mints, G. 2010. Cut-free formulations for a quantified logic of here and there. Annals of Pure and Applied Logic 162, 3, 237\u2013242.","DOI":"10.1016\/j.apal.2010.09.009"},{"key":"S1471068421000557_ref18","first-page":"294","volume-title":"Temporal Databases: Theory, Design, and Implementation","author":"Baudinet","year":"1993"},{"key":"S1471068421000557_ref25","doi-asserted-by":"crossref","unstructured":"Bozzelli, L. , Maubert, B. and Pinchinat, S. 2015. Unifying hyper and epistemic temporal logics. In Proceedings of the Eighteenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS\u201915), A. Pitts, Ed. Notes, Lecture in Computer Science, vol. 9034. Springer-Verlag, 167\u2013182.","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"S1471068421000557_ref2","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2013.798985"},{"key":"S1471068421000557_ref60","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0066"},{"key":"S1471068421000557_ref14","article-title":"Intuitionistic linear temporal logics","volume":"2","author":"Balbiani","year":"2020","journal-title":"ACM Transactions on Computational Logic 21"}],"container-title":["Theory and Practice of Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S1471068421000557","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,14]],"date-time":"2022-12-14T10:27:07Z","timestamp":1671013627000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S1471068421000557\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,27]]},"references-count":112,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1]]}},"alternative-id":["S1471068421000557"],"URL":"https:\/\/doi.org\/10.1017\/s1471068421000557","relation":{},"ISSN":["1471-0684","1475-3081"],"issn-type":[{"value":"1471-0684","type":"print"},{"value":"1475-3081","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,12,27]]},"assertion":[{"value":"\u00a9 The Author(s), 2021. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}