Hostname: page-component-78c5997874-s2hrs Total loading time: 0 Render date: 2024-11-16T15:31:18.910Z Has data issue: false hasContentIssue false
  • English
  • Français

Linear-Time Temporal Answer Set Programming

Published online by Cambridge University Press:  27 December 2021

FELICIDAD AGUADO ,
PEDRO CABALAR Open the ORCID record for PEDRO CABALAR [Opens in a new window] ,
MARTÍN DIÉGUEZ Open the ORCID record for MARTÍN DIÉGUEZ [Opens in a new window] ,
GILBERTO PÉREZ ,
TORSTEN SCHAUB Open the ORCID record for TORSTEN SCHAUB [Opens in a new window] ,
ANNA SCHUHMANN  and
CONCEPCIÓN VIDAL
FELICIDAD AGUADO
Affiliation:
University of Corunna, Spain (e-mails: [email protected], [email protected])
PEDRO CABALAR
Affiliation:
University of Corunna, Spain (e-mails: [email protected], [email protected])
MARTÍN DIÉGUEZ
Affiliation:
Université d’Angers, France (e-mail: [email protected])
GILBERTO PÉREZ
Affiliation:
University of Corunna, Spain (e-mail: [email protected])
TORSTEN SCHAUB
Affiliation:
University of Potsdam, Germany (e-mails: [email protected], [email protected])
ANNA SCHUHMANN
Affiliation:
University of Potsdam, Germany (e-mails: [email protected], [email protected])
CONCEPCIÓN VIDAL
Affiliation:
University of Corunna, Spain (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 Linear-time Temporal Logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium Logic, 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 (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.

Keywords

answer set programminglinear-time temporal logicequilibrium logicnon-monotonic reasoning
Type
Survey Article
Information
Theory and Practice of Logic Programming , Volume 23 , Issue 1 , January 2023 , pp. 2 - 56
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
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.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Abadi, M. and Manna, Z. 1989. Temporal logic programming. Journal of Symbolic Computation 8, 277–295.10.1016/S0747-7171(89)80070-7CrossRefGoogle Scholar
Aguado, F., Cabalar, P., Diéguez, M., Pérez, G. and Vidal, C. 2013. Temporal equilibrium logic: A survey. Journal of Applied Non-Classical Logics 23, 1–2, 2–24.10.1080/11663081.2013.798985CrossRefGoogle Scholar
Aguado, F., Cabalar, P., Diéguez, M., Pérez, G. and Vidal, C. 2017. Temporal equilibrium logic with past operators. Journal of Applied Non-Classical Logics 27, 3–4, 161–177.10.1080/11663081.2018.1427987CrossRefGoogle Scholar
Aguado, F., Cabalar, P., Fandinno, J., Pérez, G. and Vidal, C. 2020. Explicit negation in linear-dynamic equilibrium logic. In Proceedings of the Twenty-fourth European Conference on Artificial Intelligence (ECAI’20), De Giacomo, G., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarn, A. and Lang, J., Eds. IOS Press, 569–576.Google Scholar
Aguado, F., Cabalar, P., Pearce, D., Pérez, G. and Vidal, C. 2015. A denotational semantics for equilibrium logic. Theory and Practice of Logic Programming 15, 4–5, 620–634.10.1017/S1471068415000277CrossRefGoogle Scholar
Aguado, F., Cabalar, P., Pérez, G., Vidal, C. and Diéguez, M. 2017. Temporal logic programs with variables. Theory and Practice of Logic Programming 17, 2, 226–243.CrossRefGoogle Scholar
Aguado, F., Pérez, 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’13), Cabalar, P. and Son, T., Eds. Lecture Notes in Artificial Intelligence, vol. 8148. Springer-Verlag, 23–35.Google Scholar
Allen, J. 1983. Maintaining knowledge about temporal intervals. Communications of the ACM 26, 11, 832–843.Google Scholar
Artale, A. and Franconi, E. 2000. A survey of temporal extensions of description logics. Annals of Mathematics and Artificial Intelligence 30, 1–4, 171–210.CrossRefGoogle Scholar
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–388.Google Scholar
Baader, F., Calvanese, D., McGuinness, D., Nardi, D. and Patel-Schneider, P., Eds. 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press.Google Scholar
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’08), Brewka, G. and Lang, J., Eds. AAAI Press, 684–694.Google Scholar
Bacchus, F. and Kabanza, F. 2000. Using temporal logics to express search control knowledge for planning. Artificial Intelligence 116, 1–2, 123–191.CrossRefGoogle Scholar
Balbiani, P., Boudou, J., Diéguez, M. and Fernández-Duque, D. 2020. Intuitionistic linear temporal logics. ACM Transactions on Computational Logic 21, 2, 14:1–14:32.Google Scholar
Balbiani, P. and Diéguez, M. 2016. Temporal here and there. In Proceedings of the Fifteenth European Conference on Logics in Artificial Intelligence (JELIA’16), Michael, L. and Kakas, A., Eds. Lecture Notes in Artificial Intelligence, vol. 10021. Springer-Verlag, 81–96.Google Scholar
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’96), Dix, J., Pereira, L., and Przymusinski, T., Eds. Lecture Notes in Computer Science, vol. 1216. Springer-Verlag, 132–150.Google Scholar
Baudinet, M. 1992. A simple proof of the completeness of temporal logic programming. In Fariñas del Cerro, L. and Penttonen, M., Eds. Clarendon Press, 51–83.Google Scholar
Baudinet, M., Chomicki, J. and Wolper, P. 1993. Temporal deductive databases. In Temporal Databases: Theory, Design, and Implementation, Tansel, A., Clifford, J., Gadia, S., Segev, A. and Snodgrass, R., Eds. Benjamin/Cummings, 294–320.Google Scholar
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’16), R. Kambhampati, Ed. IJCAI/AAAI Press, 929–935.Google Scholar
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’15), Bonet, B. and Koenig, S., Eds. AAAI Press, 1431–1438.Google Scholar
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’01), B. Nebel, Ed. Morgan Kaufmann Publishers, 473–478.Google Scholar
Bieber, P., Fariñas del Cerro, L. and Herzig, A. 1988. MOLOG: a modal PROLOG. In Proceedings of the Nineth International Conference on Automated Deduction (CADE’88), Lusk, E. and Overbeek, R., Eds. Lecture Notes in Computer Science, vol. 310. Springer-Verlag, 762–763.Google Scholar
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’99), R. Cleaveland, Ed. Notes, Lecture in Computer Science, vol. 1579. Springer-Verlag, 193–207.Google Scholar
Bosser, A., Cabalar, P., Diéguez, 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’18), Thielscher, M., Toni, F., and Wolter, F., Eds. AAAI Press, 12–21.Google Scholar
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’15), A. Pitts, Ed. Notes, Lecture in Computer Science, vol. 9034. Springer-Verlag, 167–182.Google Scholar
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’15). IEEE Computer Society Press, 645–656.Google Scholar
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’16), Carro, M. and King, A., Eds. OpenAccess Series in Informatics (OASIcs), vol. 52. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 4:1–4:15.Google Scholar
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–677.Google Scholar
Brzoska, C. 1995. Temporal logic programming in dense time. In Proceedings of the International Symposium on Logic Programming, J. Lloyd, Ed. Press, MIT, 303–317.Google Scholar
Büchi, 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–11.Google Scholar
Cabalar, P. 1999. Temporal answer sets. In Proceedings of the Joint Conference on Declarative Programming (AGP’99), Meo, M. and Ferro, M., Eds, 351–366.Google Scholar
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’11), G. Vidal, Ed. Notes, Lecture in Computer Science, vol. 7225. Springer-Verlag, 57–72.Google Scholar
Cabalar, P. and Diéguez, M. 2011. STELP — A tool for temporal answer set programming. In Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’11), Delgrande, J. and Faber, W., Eds. Lecture Notes in Artificial Intelligence, vol. 6645. Springer-Verlag, 370–375.Google Scholar
Cabalar, P. and Diéguez, M. 2014. Strong equivalence of non-monotonic temporal theories. In Proceedings of the Fourteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’14), Baral, C., De Giacomo, G. and Eiter, T., Eds. AAAI Press.Google Scholar
Cabalar, P., Diéguez, 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’20), De Giacomo, G., Catalá, A., Dilkina, B., Milano, M., Barro, S., Bugarn, A. and Lang, J., Eds. IOS Press, 656–663.Google Scholar
Cabalar, P., Diéguez, M., Schaub, T. and Schuhmann, A. 2020. Towards metric temporal answer set programming. Theory and Practice of Logic Programming 20, 5, 783–798.CrossRefGoogle Scholar
Cabalar, P., Diéguez, M., and Vidal, C. 2015. An infinitary encoding of temporal equilibrium logic. Theory and Practice of Logic Programming 15, 4–5, 666–680.CrossRefGoogle Scholar
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’19), Balduccini, M., Lierler, Y., and Woltran, S., Eds. Lecture Notes in Artificial Intelligence, vol. 11481. Springer-Verlag, 256–269.Google Scholar
Cabalar, P., Kaminski, R., Schaub, T. and Schuhmann, A. 2018. Temporal answer set programming on finite traces. Theory and Practice of Logic Programming 18, 3–4, 406–420.10.1017/S1471068418000297CrossRefGoogle Scholar
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’19), Oliveira, P., Novais, P., and Reis, L., Eds. Lecture Notes in Computer Science, vol. 11805. Springer, 520–525.Google Scholar
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–186.Google Scholar
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’17), Moreno-Daz, R., Pichler, F. and Quesada-Arencibia, A., Eds. Lecture Notes in Computer Science, vol. 4739. Springer-Verlag, 241–248.Google Scholar
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’18), de Weerdt, M., Koenig, S., Röger, G. and Spaan, M., Eds. AAAI Press, 29–38.Google Scholar
Castilho, M., Gasquet, O. and Herzig, A. 1999. Formalizing action and change in modal logic I: the frame problem. Journal of Logic and Computation 9, 5, 701–735.CrossRefGoogle Scholar
Chandra, A., Kozen, D. and Stockmeyer, L. 1981. Alternation. Journal of the ACM 28, 1, 114–133.CrossRefGoogle Scholar
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–73.Google Scholar
Chomicki, J. and Imielinski, T. 1993. Finite representation of infinite query answers. ACM Transactions on Database Systems 18, 2, 181–223.CrossRefGoogle Scholar
de Bruijn, J., Pearce, D., Polleres, A. and Valverde, A. 2010. A semantical framework for hybrid knowledge bases. Knowledge Information Systems 25, 1, 81–104.10.1007/s10115-010-0294-zCrossRefGoogle Scholar
De Giacomo, G. and Perelli, G. 2021. Behavioral QLTL. CoRR abs/2102.11184.Google Scholar
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’13), F. Rossi, Ed. IJCAI/AAAI Press, 854–860.Google Scholar
Demri, S., Goranko, V. and Lange, M. 2016. Temporal Logics in Computer Science: Finite-State Systems . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.Google Scholar
Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E. and Xu, L. 2016. Spot 2.0 – A framework for LTL and $\omega$ -automata manipulation. In Proceedings of Fourteenth International Symposium on Automated Technology for Verification and Analysis (ATVA’16), Artho, C., Legay, A. and Peled, D., Eds. Lecture Notes in Computer Science, vol. 9938. 122–129.Google Scholar
Eiter, T. and Šimkus, M. 2009. Bidirectional answer set programs with function symbols. In Proceedings of the Twenty-first International Joint Conference on Artificial Intelligence (IJCAI’09), C. Boutilier, Ed. AAAI/MIT Press, 765–771.Google Scholar
Fages, F. 1994. Consistency of Clark’s completion and the existence of stable models. Journal of Methods of Logic in Computer Science 1, 51–60.Google Scholar
Fariñas del Cerro, L. 1986. MOLOG: A system that extends PROLOG with modal logic. New Generation Computing 4, 1, 35–50.10.1007/BF03037381CrossRefGoogle Scholar
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’07), M. Veloso, Ed. AAAI/MIT Press, 372–379.Google Scholar
Fischer, M. and Ladner, R. 1979. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences 18, 2, 194–211.CrossRefGoogle Scholar
Fisher, M. 1994. A survey of concurrent METATEM – The language and its applications. In Proceedings of the First International Conference on Temporal Logic (ICTL’94), Gabbay, D. and Ohlbach, H., Eds. Lecture Notes in Computer Science, vol. 827. Springer-Verlag, 480–505.Google Scholar
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’s College Publications, 127–148.Google Scholar
Frühwirth, T. 1996. Temporal annotated constraint logic programming. Journal of Symbolic Computation 22, 5–6, 555–583.CrossRefGoogle Scholar
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’86), E. Shapiro, Ed. Notes, Lecture in Computer Science, vol. 225. Springer, 695–709.Google Scholar
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–448.Google Scholar
Gabbay, D. 1987b. Modal and temporal logic programming. In Temporal Logics and their Applications, A. Galton, Ed. Press, Academic, Chapter 6, 197–237.Google Scholar
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’80), Abrahams, P., Lipton, R. and Bourne, S., Eds. ACM Press, 163–173.Google Scholar
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–82.Google Scholar
Gelfond, M. and Lifschitz, V. 1988. Compiling circumscriptive theories into logic programs. In Proceedings of the Seventh National Conference on Artificial Intelligence (AAAI’88), Shrobe, H., Mitchell, T. and Smith, R., Eds. AAAI Press/The MIT Press, 455–459.Google Scholar
Gelfond, M. and Lifschitz, V. 1993. Representing action and change by logic programs. Journal of Logic Programming 17, 2–4, 301–321.CrossRefGoogle Scholar
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–18.Google Scholar
Giordano, L., Martelli, A. and Dupré, 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’12), Brewka, G., Eiter, T. and McIlraith, S., Eds. AAAI Press.Google Scholar
Giordano, L., Martelli, A. and Theseider Dupré, D. 2013. Reasoning about actions with temporal answer sets. Theory and Practice of Logic Programming 13, 2, 201–225.CrossRefGoogle Scholar
Giordano, L., Martelli, M. and Schwind, C. 2001. Reasoning about actions in dynamic linear time temporal logic. Logic Journal of the IGPL 9, 2, 273–288.CrossRefGoogle Scholar
Gödel, K. 1932. Zum intuitionistischen Aussagenkalkül. Anzeiger der Akademie der Wissenschaften in Wien, 65–66.Google Scholar
Goldblatt, R. 1992. Logics of Time and Computation. Number 7 in CSLI Lecture Notes. Center for the Study of Language and Information.Google Scholar
Gottlob, G., Grädel, E. and Veith, H. 2002. Datalog LITE: A deductive query language with linear time model checking. ACM Transactions on Computational Logic 3, 1, 42–79.CrossRefGoogle Scholar
Guessarian, I., Foustoucos, E., Andronikos, T. and Afrati, F. 2003. On temporal logic versus datalog. Theoretical Computer Science 303, 1, 103–133.CrossRefGoogle Scholar
Harel, D., Tiuryn, J. and Kozen, D. 2000. Dynamic Logic. MIT Press.CrossRefGoogle Scholar
Heljanko, K. and Niemelä, I. 2003. Bounded LTL model checking with stable models. Theory and Practice of Logic Programming 3, 4–5, 519–550.CrossRefGoogle Scholar
Henriksen, J., Jensen, J., Jørgensen, 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’95), Brinksma, E., Cleaveland, R., Larsen, K., Margaria, T. and Steffen, B., Eds. Lecture Notes in Computer Science, vol. 1019. Springer-Verlag, 89–110.Google Scholar
Henriksen, J. and Thiagarajan, P. 1999. Dynamic linear time temporal logic. Annals Pure and Applied Logic 96, 1–3, 187–207.CrossRefGoogle Scholar
Heyting, A. 1930. Die formalen Regeln der intuitionistischen Logik. In Sitzungsberichte der Preussischen Akademie der Wissenschaften. Deutsche Akademie der Wissenschaften zu Berlin, 42–56.Google Scholar
Hosoi, T. 1966. The axiomatization of the intermediate propositional systems $s_2$ of Gödel. Journal of the Faculty of Science of the University of Tokyo 13, 2, 183–187.Google Scholar
Hrycej, T. 1988. Temporal Prolog. In Proceedings of the Eighth European Conference on Artificial Intelligence (ECAI’92), Y. Kodratoff, Ed. Pitman/Morgan Kaufmann, 296–301.Google Scholar
Kamp, J. 1968. Tense logic and the theory of linear order. Ph.D. thesis, University of California at Los Angeles.Google Scholar
Kvarnström, 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’08), Rintanen, J., Nebel, B., Beck, J. and Hansen, E., Eds. AAAI Press, 198–205.Google Scholar
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’13), F. Rossi, Ed. IJCAI/AAAI Press, 983–989.Google Scholar
Levesque, H., Reiter, R., Lespérance, Y., Lin, F. and Scherl, R. 1997. GOLOG: A logic programming language for dynamic domains. Journal of Logic Programming 31, 1–3, 59–83.CrossRefGoogle Scholar
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’12). IEEE Computer Society Press, 603–609.Google Scholar
Lifschitz, V. 2002. Answer set programming and plan generation. Artificial Intelligence 138, 1–2, 39–54.CrossRefGoogle Scholar
Lukasiewicz, J. 1941. Die logik und das grundlagenproblem. Les Entreties de Zürich sur les Fondaments et la Méthode des Sciences Mathématiques 12, 6–9, 82–100.Google Scholar
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’08), Demri, S. and Jensen, C., Eds. IEEE Computer Society Press, 3–14.Google Scholar
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.Google Scholar
Mints, G. 2010. Cut-free formulations for a quantified logic of here and there. Annals of Pure and Applied Logic 162, 3, 237–242.Google Scholar
Moszkowski, B. 1986. Executing Temporal Logic Programs. Cambridge University Press.Google Scholar
Oikarinen, E. and Janhunen, T. 2006. Modular equivalence for normal logic programs. In Proceedings of the Seventeenth European Conference on Artificial Intelligence (ECAI’06), Brewka, G., Coradeschi, S., Perini, A. and Traverso, P., Eds. IOS Press, 412–416.Google Scholar
Orgun, M. and Wadge, W. 1990. Theory and practice of temporal logic programming. Fariñas del Cerro, L. and Penttonen, M., Eds. Clarendon Press, 21–50.Google Scholar
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’96), Dix, J., Pereira, L. and Przymusinski, T., Eds. Lecture Notes in Computer Science, vol. 1216. Springer-Verlag, 57–70.Google Scholar
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’01), Brazdil, P. and Jorge, A., Eds. Lecture Notes in Computer Science, vol. 2258. Springer-Verlag, 306–320.Google Scholar
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’08), Garcia De La Banda, M. and Pontelli, E., Eds. Lecture Notes in Computer Science, vol. 5366. Springer-Verlag, 546–560.Google Scholar
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’01), B. Nebel, Ed. Morgan Kaufmann Publishers, 479–486.Google Scholar
Pnueli, A. 1977. The temporal logic of programs. In Proceedings of the Eight-teenth Symposium on Foundations of Computer Science (FOCS’77). IEEE Computer Society Press, 46–57.Google Scholar
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évy, J. and Vallduví, E., Eds. 275–291.Google Scholar
Simpson, A. 1994. The Proof Theory and Semantics of Intuitionistic Modal Logic. Ph.D. thesis, University of Edinburgh.Google Scholar
Sistla, A. 1983. Theoretical issues in the design and verification of distributed systems. Ph.D. thesis, Harvard University.Google Scholar
Sistla, A. and Clarke, E. 1985. The complexity of propositional linear temporal logic. Journal of the ACM 32, 3, 733–749.CrossRefGoogle Scholar
Sistla, A., Vardi, M. and Wolper, P. 1987. The complementation problem for Büchi automata with appplications to temporal logic. Theoretical Computer Science 49, 217–237.CrossRefGoogle Scholar
van Dalen, D. 2001. Intuitionistic logic. In Handbook of Philosophical Logic, Gabbay, D. and Guenthner, F., Eds. Vol. 3. Springer-Verlag, 225–339.Google Scholar
van Emden, M. and Kowalski, R. 1976. The semantics of predicate logic as a programming language. Journal of the ACM 23, 4, 733–742.CrossRefGoogle Scholar
Wałega, 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’19), S. Kraus, Ed. ijcai.org, 1886–1892.Google Scholar
Wałega, 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’22), Bienvenu, M., Lakemeyer, G., and Erdem, E., Eds. AAAI Press, 609–618.Google Scholar
Wolper, P. 1983. Temporal logic can be more expressive. Information and Control 56, 1/2, 72–99.Google Scholar
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’19), Gopal, T. and Watada, J., Eds. Lecture Notes in Computer Science, vol. 11436. Springer-Verlag, 684–705.Google Scholar
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’17), C. Sierra, Ed. IJCAI/AAAI Press, 1362–1369.Google Scholar