Abstract
This work makes an overview on an hybrid formalism that combines the syntax of Linear-time Temporal Logic (LTL) with a non-monotonic selection of models based on Equilibrium Logic. The resulting approach, called Temporal Equilibrium Logic, extends the concept of a stable model for any arbitrary modal temporal theory, constituting a suitable formal framework for the specification and verification of dynamic scenarios in Answer Set Programming (ASP). We will recall the basic definitions of this logic and explain their effects on some simple examples. After that, we will proceed to summarize the advances made so far, both in the fundamental realm and in the construction of reasoning tools. Finally, we will explain some open topics, many of them currently under study, and foresee potential challenges for future research.
This research was partially supported by Spanish MEC project TIN2013-42149-P and Xunta de Galicia grant GPC 2013/070.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
John McCarthy, the founder of logical knowledge representation and commonsense reasoning, showed in several occasions an explicit disapproval of modal logics. See for instance his position paper with the self-explanatory title “Modality, si! Modal logic, no!” [4].
- 2.
Generally speaking, a disjunction of the form \(\varphi \vee {not }\; \varphi \) in ASP is not a tautology. When included in a rule head it is usually written as \(\{ \ \varphi \ \}\) and acts as a non-deterministic choice possibly allowing the derivation of \(\varphi \).
- 3.
The axiomatisation of THT is currently under study [21].
- 4.
In fact, Theorem 1 in the next section shows that LTL can be encoded into TEL by adding a simple axiom schema.
- 5.
In fact, as shown in [31], this normal form can be even more restrictive: initial rules can be replaced by atoms, and we can avoid the use of literals of the form \(\lnot \!\bigcirc \!p\).
- 6.
An incorrect proof was published in [38], but we still conjecture that the result might be positive.
References
McCarthy, J., Hayes, P.J.: Some philosophical problems from the standpoint of artificial intelligence. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, pp. 463–502. Edinburgh University Press, Edinburgh (1969)
Kowalski, R., Sergot, M.: A logic-based calculus of events. New Gener. Comput. 4, 67–95 (1986)
McCarthy, J.: Circumscription: a form of non-monotonic reasoning. Artif. Intell. 13, 27–39 (1980)
Mccarthy, J.: Modality, si! modal logic, no!. Stud. Logica. 59(1), 29–32 (1997)
Castilho, M.A., Gasquet, O., Herzig, A.: Formalizing action and change in modal logic I: the frame problem. J. Logic Comput. 9(5), 701–735 (1999)
Giordano, L., Martelli, A., Schwind, C.: Ramification and causality in a modal action logic. J. Logic Comput. 10(5), 625–662 (2000)
Baral, C., Zhao, J.: Nonmonotonic temporal logics for goal specification. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), pp. 236–242 (2007)
Gelfond, M., Lifschitz, V.: Representing action and change by logic programs. J. Logic Program. 17, 301–321 (1993)
Gelfond, M., Lifschitz, V.: Action languages. Linköping Electron. Art. Comput. Inf. Sci. 3(16) (1998). http://www.ep.liu.se/ea/cis/1998/016
Niemelä, I.: Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25(3–4), 241–273 (1999)
Marek, V., Truszczyński, M.: Stable models and an alternative logic programming paradigm. In: Apt, K.R., et al. (eds.) The Logic Programming Paradigm, pp. 169–181. Springer, Heidelberg (1999)
Gebser, M., Sabuncu, O., Schaub, T.: An incremental answer set programming based system for finite model computation. AI Commun. 24(2), 195–212 (2011)
Kautz, H.A., Selman, B.: Planning as satisfiability. In: Proceedings of the European Conference on Artificial Intelligence (ECAI 1992), pp. 359–363 (1992)
Cabalar, P., Pérez Vega, G.: Temporal equilibrium logic: a first approach. In: Moreno Díaz, R., Pichler, F., Quesada Arencibia, A. (eds.) EUROCAST 2007. LNCS, vol. 4739, pp. 241–248. Springer, Heidelberg (2007)
Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Proceedings of the 5th International Conference on Logic Programming (ICLP 1988), Seattle, Washington, pp. 1070–1080 (1988)
Prior, A.: Past, Present and Future. Oxford University Press, Oxford (1967)
Kamp, H.: Tense logic and the theory of linear order. Ph.D. thesis, UCLA (1968)
Pearce, D.: A new logical characterisation of stable models and answer sets. In: Proceedings of Non-Monotonic Extensions of Logic Programming (NMELP 1996), Bad Honnef, Germany, pp. 57–70 (1996)
Heyting, A.: Die formalen Regeln der intuitionistischen Logik. Sitzungsberichte der Preussischen Akademie der Wissenschaften, Physikalisch-mathematische Klasse (1930)
Aguado, F., Cabalar, P., Diéguez, M., Pérez, G., Vidal, C.: Temporal equilibrium logic: a survey. J. Appl. Non-classical Logics 23(1–2), 2–24 (2013)
Balbiani, P., Diéguez, M.: An axiomatisation of the logic of temporal here-and-there (2015) (unpublished draft)
Büchi, J.R.: On a decision method in restricted second-order arithmetic. In: International Congress on Logic, Methodology, and Philosophy of Science, pp. 1–11 (1962)
Cabalar, P., Demri, S.: Automata-based computation of temporal equilibrium models. In: Vidal, G. (ed.) LOPSTR 2011. LNCS, vol. 7225, pp. 57–72. Springer, Heidelberg (2012)
Cabalar, P., Diéguez, M., Vidal, C.: An infinitary encoding of temporal equilibrium logic. In: Proceedings of the 31st International Conference on Logic Programming (ICLP 2015) (2015)
Harrison, A., Lifschitz, V., Pearce, D., Valverde, A.: Infinitary equilibrium logic. In: Working Notes of Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2014) (2014)
Pearce, D.J., Valverde, A.: Quantified equilibrium logic and foundations for answer set programs. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 546–560. Springer, Heidelberg (2008)
Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. Comput. Logic 2(4), 526–541 (2001)
Cabalar, P., Diéguez, M.: Strong equivalence of non-monotonic temporal theories. In: Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning (KR 2014), Vienna, Austria (2014)
Cabalar, P., Ferraris, P.: Propositional theories are strongly equivalent to logic programs. Theor. Pract. Logic Program. 7(6), 745–759 (2007)
Fisher, M.: A resolution method for temporal logic. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI 1991), pp. 99–104. Morgan Kaufmann Publishers Inc. (1991)
Cabalar, P.: A normal form for linear temporal equilibrium logic. In: Janhunen, T., Niemelä, I. (eds.) JELIA 2010. LNCS, vol. 6341, pp. 64–76. Springer, Heidelberg (2010)
Bozzelli, L., Pearce, D.: On the complexity of temporal equilibrium logic. In: Proceedings of the 30th Annual ACM/IEEE Symposium of Logic in Computer Science (LICS 2015), Kyoto, Japan (2015, to appear)
Cabalar, P., Diéguez, M.: STeLP – a tool for temporal answer set programming. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol. 6645, pp. 370–375. Springer, Heidelberg (2011)
Lifschitz, V., Turner, H.: Splitting a logic program. In: Proceedings of the 11th International Conference on Logic programming (ICLP 1994), pp. 23–37 (1994)
Aguado, F., Cabalar, P., Pérez, G., Vidal, C.: Loop formulas for splitable temporal logic programs. In: Delgrande, J.P., Faber, W. (eds.) LPNMR 2011. LNCS, vol. 6645, pp. 80–92. Springer, Heidelberg (2011)
Ferraris, P., Lee, J., Lifschitz, V.: A generalization of the Lin-Zhao theorem. Ann. Math. Artif. Intell. 47, 79–101 (2006)
Aguado, F., Cabalar, P., Diéguez, M., Pérez, G., Vidal, C.: Paving the way for temporal grounding. In: Proc. of the 28th International Conference on Logic Programming (ICLP 2012) (2012)
Cabalar, P., Diéguez, M.: Temporal stable models are LTL-representable. In: Proceedings of the 7th International Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2014) (2014)
Aguado, F., Pérez, G., Vidal, C.: Integrating temporal extensions of answer set programming. In: Cabalar, P., Son, T.C. (eds.) LPNMR 2013. LNCS, vol. 8148, pp. 23–35. Springer, Heidelberg (2013)
Bertino, E., Mileo, A., Provetti, A.: PDL with preferences. In: 6th IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY 2005), pp. 213–222 (2005)
Acknowledgements
This research is part of a long term project developed during the last eight years in the KR group from the University of Corunna and, especially, in close cooperation with Felicidad Aguado, Martín Diéguez, Gilberto Pérez and Concepción Vidal together with the regular collaborators David Pearce and Luis Fariñas. I am also especially thankful to Stèphane Demri, Philippe Balbiani, Andreas Herzig, Laura Bozzelli, Manuel Ojeda, Agustín Valverde, Stefania Costantini, Michael Fisher, Mirosław Truszczyński, Vladimir Lifschitz and Torsten Schaub for their useful discussions and collaboration at different moments on specific topics of this work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Cabalar, P. (2015). Stable Models for Temporal Theories. In: Calimeri, F., Ianni, G., Truszczynski, M. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2015. Lecture Notes in Computer Science(), vol 9345. Springer, Cham. https://doi.org/10.1007/978-3-319-23264-5_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-23264-5_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-23263-8
Online ISBN: 978-3-319-23264-5
eBook Packages: Computer ScienceComputer Science (R0)