×

First-order stable model semantics with intensional functions. (English) Zbl 1478.68341

Summary: In classical logic, nonBoolean fluents, such as the location of an object, can be naturally described by functions. However, this is not the case in answer set programs, where the values of functions are pre-defined, and nonmonotonicity of the semantics is related to minimizing the extents of predicates but has nothing to do with functions. We extend the first-order stable model semantics by Ferraris, Lee, and Lifschitz to allow intensional functions – functions that are specified by a logic program just like predicates are specified. We show that many known properties of the stable model semantics are naturally extended to this formalism and compare it with other related approaches to incorporating intensional functions. Furthermore, we use this extension as a basis for defining Answer Set Programming Modulo Theories (ASPMT), analogous to the way that Satisfiability Modulo Theories (SMT) is defined, allowing for SMT-like effective first-order reasoning in the context of Answer Set Programming (ASP). Using SMT solving techniques involving functions, ASPMT can be applied to domains containing real numbers and alleviates the grounding problem. We show that other approaches to integrating ASP and CSP/SMT can be related to special cases of ASPMT in which functions are limited to non-intensional ones.

MSC:

68T27 Logic in artificial intelligence
68N17 Logic programming
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Asuncion, Vernon; Chen, Yin; Zhang, Yan; Zhou, Yi, Ordered completion for logic programs with aggregates, Artif. Intell., 224, 72-102, (2015) · Zbl 1343.68043
[2] Babb, Joseph; Lee, Joohyung, Cplus2ASP: computing action language \(\mathcal{C} +\) in answer set programming, (Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), (2013)), 122-134 · Zbl 1405.68041
[3] Balduccini, Marcello, Representing constraint satisfaction problems in answer set programming, (Working Notes of the Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP), (2009)) · Zbl 1219.68083
[4] Balduccini, Marcello, A “conservative” approach to extending answer set programming with non-Herbrand functions, (Correct Reasoning - Essays on Logic-Based AI in Honour of Vladimir Lifschitz, (2012)), 24-39 · Zbl 1248.68468
[5] Barrett, Clark W.; Sebastiani, Roberto; Seshia, Sanjit A.; Tinelli, Cesare, Satisfiability modulo theories, (Biere, Armin; Heule, Marijn; van Maaren, Hans; Walsh, Toby, Frontiers in Artificial Intelligence and Applications. Frontiers in Artificial Intelligence and Applications, Handbook of Satisfiability, vol. 185, (2009), IOS Press), 825-885
[6] Bartholomew, Michael; Lee, Joohyung, Stable models of formulas with intensional functions, (Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), (2012)), 2-12
[7] Bartholomew, Michael; Lee, Joohyung, Functional stable model semantics and answer set programming modulo theories, (Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), (2013)) · Zbl 1286.68041
[8] Bartholomew, Michael; Lee, Joohyung, A functional view of strong negation, (Working Notes of the 5th Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP), (2013))
[9] Bartholomew, Michael; Lee, Joohyung, On the stable model semantics for intensional functions, Theory Pract. Log. Program., 13, 4-5, 863-876, (2013) · Zbl 1286.68041
[10] Bartholomew, Michael; Lee, Joohyung, System ASPMT2SMT: computing ASPMT theories by SMT solvers, (Proceedings of European Conference on Logics in Artificial Intelligence (JELIA), (2014)), 529-542 · Zbl 1432.68055
[11] Brewka, Gerhard; Niemelä, Ilkka; Truszczynski, Miroslaw, Answer set programming at a glance, Commun. ACM, 54, 12, 92-103, (2011)
[12] Cabalar, Pedro, Functional answer set programming, Theory Pract. Log. Program., 11, 2-3, 203-233, (2011) · Zbl 1220.68033
[13] Clark, Keith, Negation as failure, (Gallaire, Herve; Minker, Jack, Logic and Data Bases, (1978), Plenum Press: Plenum Press New York), 293-322
[14] Ferraris, Paolo; Lee, Joohyung; Lifschitz, Vladimir, A new perspective on stable models, (Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), (2007)), 372-379
[15] Ferraris, Paolo; Lee, Joohyung; Lifschitz, Vladimir; Palla, Ravi, Symmetric splitting in the general theory of stable models, (Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), (2009), AAAI Press), 797-803
[16] Ferraris, Paolo; Lee, Joohyung; Lifschitz, Vladimir, Stable models and circumscription, Artif. Intell., 175, 236-263, (2011) · Zbl 1227.68103
[17] Fox, Maria; Long, Derek, PDDL2.1: an extension to PDDL for expressing temporal planning domains, J. Artif. Intell. Res., 20, 61-124, (2003) · Zbl 1036.68093
[18] Fox, Maria; Long, Derek, Modelling mixed discrete-continuous domains for planning, J. Artif. Intell. Res., 27, 235-297, (2006) · Zbl 1182.68238
[19] Gao, Sicun; Kong, Soonho; Clarke, Edmund, Satisfiability modulo ODEs, (2013), arXiv preprint
[20] Gao, Sicun; Kong, Soonho; Clarke, Edmund M., dReal: an SMT solver for nonlinear theories over the reals, (International Conference on Automated Deduction, (2013), Springer: Springer Berlin, Heidelberg), 208-214 · Zbl 1381.68268
[21] Gebser, M.; Ostrowski, M.; Schaub, T., Constraint answer set solving, (Proceedings of International Conference on Logic Programming (ICLP), (2009)), 235-249 · Zbl 1251.68061
[22] Gelfond, Michael; Kahl, Yulia, Knowledge Representation, Reasoning, and the Design of Intelligent Agents, (2014), Cambridge University Press
[23] Gelfond, Michael; Lifschitz, Vladimir, The stable model semantics for logic programming, (Kowalski, Robert; Bowen, Kenneth, Proceedings of International Logic Programming Conference and Symposium, (1988), MIT Press), 1070-1080
[24] Giunchiglia, Enrico; Lee, Joohyung; Lifschitz, Vladimir; McCain, Norman; Turner, Hudson, Nonmonotonic causal theories, Artif. Intell., 153, 1-2, 49-104, (2004) · Zbl 1085.68161
[25] Janhunen, Tomi; Liu, Guohua; Niemelä, Ilkka, Tight integration of non-ground answer set programming and satisfiability modulo theories, (Working Notes of the 1st Workshop on Grounding and Transformations for Theories with Variables, (2011)) · Zbl 1326.68058
[26] Lee, Joohyung; Meng, Yunsong, Answer set programming modulo theories and reasoning about continuous changes, (Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), (2013))
[27] Lee, Joohyung; Lifschitz, Vladimir; Yang, Fangkai, Action language \(\mathcal{BC}\): preliminary report, (Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), (2013))
[28] Lee, Joohyung; Loney, Nikhil; Meng, Yunsong, Representing hybrid automata by action language modulo theories, (Theory and Practice of Logic Programming, (2017)) · Zbl 1422.68154
[29] Lierler, Yuliya; Susman, Benjamin, Constraint answer set programming versus satisfiability modulo theories, (IJCAI, (2016)), 1181-1187 · Zbl 1379.68285
[30] Lifschitz, Vladimir; Turner, Hudson, Representing transition systems by logic programs, (Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), (1999)), 92-106 · Zbl 0952.68132
[31] Lifschitz, Vladimir; Yang, Fangkai, Eliminating function symbols from a nonmonotonic causal theory, (Lakemeyer, Gerhard; McIlraith, Sheila A., Knowing, Reasoning, and Acting: Essays in Honour of Hector J. Levesque, (2011), College Publications) · Zbl 1341.68215
[32] Lifschitz, Vladimir; Yang, Fangkai, Functional completion, J. Appl. Non-Class. Log., 23, 1-2, 121-130, (2013) · Zbl 1400.68205
[33] Lifschitz, Vladimir; Pearce, David; Valverde, Agustin, Strongly equivalent logic programs, ACM Trans. Comput. Log., 2, 526-541, (2001) · Zbl 1365.68149
[34] Lifschitz, Vladimir, On the declarative semantics of logic programs with negation, (Minker, Jack, Foundations of Deductive Databases and Logic Programming, (1988), Morgan Kaufmann: Morgan Kaufmann San Mateo, CA), 177-192
[35] Lifschitz, Vladimir, Circumscription, (Gabbay, D. M.; Hogger, C. J.; Robinson, J. A., Handbook of Logic in AI and Logic Programming, vol. 3, (1994), Oxford University Press), 298-352
[36] Lifschitz, Vladimir, On the logic of causal explanation, Artif. Intell., 96, 451-465, (1997) · Zbl 0901.03022
[37] Lifschitz, Vladimir, What is answer set programming?, (Proceedings of the AAAI Conference on Artificial Intelligence, (2008), MIT Press), 1594-1597
[38] Lifschitz, Vladimir, Datalog programs and their stable models, (de Moor, O.; Gottlob, G.; Furche, T.; Sellers, A., Datalog Reloaded: First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010. Datalog Reloaded: First International Workshop, Datalog 2010, Oxford, UK, March 16-19, 2010, Revised Selected Papers, (2011), Springer) · Zbl 1287.68021
[39] Lifschitz, Vladimir, Logic programs with intensional functions, (Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), (2012)), 24-31
[40] Lin, Fangzhen; Wang, Yisong, Answer set programming with functions, (Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), (2008)), 454-465
[41] Lin, Fangzhen, Embracing causality in specifying the indirect effects of actions, (Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), (1995)), 1985-1991
[42] Liu, Guohua; Janhunen, Tomi; Niemelä, Ilkka, Answer set programming via mixed integer programming, (Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), (2012)), 32-42
[43] McCarthy, John, Circumscription—a form of non-monotonic reasoning, Artif. Intell., 13, 27-39, 171-172, (1980) · Zbl 0435.68072
[44] Mellarkod, Veena S.; Gelfond, Michael; Zhang, Yuanlin, Integrating answer set programming and constraint logic programming, Ann. Math. Artif. Intell., 53, 1-4, 251-287, (2008) · Zbl 1165.68504
[45] Wałega, Przemysław Andrzej; Bhatt, Mehul; Schultz, Carl, ASPMT(QS): non-monotonic spatial reasoning with answer set programming modulo theories, (Logic Programming and Nonmonotonic Reasoning, (2015), Springer), 488-501 · Zbl 1470.68219
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.