×

zbMATH — the first resource for mathematics

A progression semantics for first-order logic programs. (English) Zbl 1419.68035
Summary: In this paper, we propose a progression semantics for first-order normal logic programs, and show that it is equivalent to the well-known stable model (answer set) semantics. The progressional definition sheds new insights into Answer Set Programming (ASP), for instance, its relationships to Datalog, First-Order Logic (FOL) and Satisfiability Modulo Theories (SMT). As an example, we extend the notion of boundedness in Datalog for ASP, and show that it coincides with the notions of recursion-freeness and loop-freeness under program equivalence. In addition, we prove that boundedness precisely captures first-order definability for normal logic programs on arbitrary structures. Finally, we show that the progressional definition suggests an alternative translation from ASP to SMT, which yields a new way of implementing first-order ASP.
MSC:
68N17 Logic programming
68Q55 Semantics in the theory of computing
Software:
ASSAT; Cmodels
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abiteboul, Serge; Hull, Richard; Vianu, Victor, Foundations of databases, (1995), Addison-Wesley · Zbl 0848.68031
[2] Ajtai, Miklós; Gurevich, Yuri, Datalog vs first-order logic, J. Comput. Syst. Sci., 49, 3, 562-588, (1994) · Zbl 0824.68034
[3] Asuncion, Vernon; Chen, Yin; Zhang, Yan; Zhou, Yi, Ordered completion for logic programs with aggregates, Artif. Intell., 224, 72-102, (2015) · Zbl 1343.68043
[4] Asuncion, Vernon; Lin, Fangzhen; Zhang, Yan; Zhou, Yi, Ordered completion for first-order logic programs on finite structures, Artif. Intell., 177-179, 1-24, (2012) · Zbl 1244.68072
[5] Asuncion, Vernon; Zhang, Yan; Zhou, Yi, Ordered completion for logic programs with aggregates, (AAAI-2012, (2012)), 691-697
[6] Baral, Chitta, Knowledge representation, reasoning and declarative problem solving, (2003), Cambridge University Press · Zbl 1056.68139
[7] Bartholomew, Michael; Lee, Joohyung, Functional stable model semantics and answer set programming modulo theories, (IJCAI 2013, (2013)) · Zbl 1286.68041
[8] 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
[9] Bartholomew, Michael; Lee, Joohyung, Stable models of multi-valued formulas: partial versus total functions, (Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, July 20-24, 2014, (2014))
[10] Bartholomew, Michael; Lee, Joohyung; Meng, Yunsong, First-order extension of the FLP stable model semantics via modified circumscription, (IJCAI-2011, (2011)), 724-730
[11] Barwise, J.; Moschovakis, Y., Global inductive definability, J. Symb. Log., 43, 521-534, (1978) · Zbl 0395.03021
[12] Chen, Yin; Lin, Fangzhen; Wang, Yisong; Zhang, Mingyi, First-order loop formulas for normal logic programs, (Proceedings, Tenth International Conference on Principles of Knowledge Representation and Reasoning, Lake District of the United Kingdom, June 2-5, 2006, (2006)), 298-307
[13] Chen, Yin; Lin, Fangzhen; Zhang, Yan; Zhou, Yi, Loop-separable programs and their first-order definability, Artif. Intell., 175, 3-4, 890-913, (2011) · Zbl 1223.68027
[14] Clark, Keith L., Negation as failure, (Logics and Databases, (1978)), 293-322
[15] Denecker, Marc; Lierler, Yuliya; Truszczynski, Miroslaw; Vennekens, Joost, A Tarskian informal semantics for answer set programming, (ICLP 2012, (2012)), 277-289 · Zbl 1281.68147
[16] Ebbinghaus, Heinz-Dieter; Flum, Jörg, Finite model theory, Perspectives in Mathematical Logic, (1995), Springer · Zbl 0841.03014
[17] Fages, François, Consistency of Clark’s completion and existence of stable models, Meth. of Logic in CS, 1, 1, 51-60, (1994)
[18] Ferraris, Paolo; Lee, Joohyung; Lifschitz, Vladimir, Stable models and circumscription, Artif. Intell., 175, 1, 236-263, (2011) · Zbl 1227.68103
[19] Gaifman, Haim; Mairson, Harry G.; Sagiv, Yehoshua; Vardi, Moshe Y., Undecidable optimization problems for database logic programs, J. ACM, 40, 3, 683-713, (1993) · Zbl 0785.68021
[20] Gebser, Martin; Kaminski, Roland; Kaufmann, Benjamin; Schaub, Torsten, Answer set solving in practice, Synthesis Lectures on Artificial Intelligence and Machine Learning, (2012), Morgan & Claypool Publishers · Zbl 1251.68060
[21] Gelfond, Michael; Lifschitz, Vladimir, The stable model semantics for logic programming, (Proceedings of International Logic Programming Conference and Symposium, (1988), MIT Press), 1070-1080
[22] Gelfond, Michael; Lifschitz, Vladimir, Classical negation in logic programs and disjunctive databases, New Gener. Comput., 9, 3/4, 365-386, (1991) · Zbl 0735.68012
[23] Gottlob, Georg; Hernich, André; Kupke, Clemens; Lukasiewicz, Thomas, Stable model semantics for guarded existential rules and description logics, (Principles of Knowledge Representation and Reasoning: Proceedings of the Fourteenth International Conference, KR 2014, Vienna, Austria, July 20-24, 2014, (2014))
[24] Harrison, Amelia; Lifschitz, Vladimir; Pearce, David; Valverde, Agustín, Infinitary equilibrium logic and strongly equivalent logic programs, Artif. Intell., 246, 22-33, (2017) · Zbl 1419.68120
[25] Janhunen, Tomi; Niemela, Ilkka, Compact translations of non-disjunctive answer set programs to propositional clauses, (Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning - Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday, (2011)), 111-130 · Zbl 1326.68058
[26] Lee, Joohyung; Meng, Yunsong, First-order stable model semantics and first-order loop formulas, J. Artif. Intell. Res., 42, 125-180, (2011) · Zbl 1234.68247
[27] Lierler, Yuliya, Cmodels - SAT-based disjunctive answer set solver, (Logic Programming and Nonmonotonic Reasoning, 8th International Conference, LPNMR 2005, Diamante, Italy, September 5-8, 2005, Proceedings, (2005)), 447-451
[28] Lifschitz, Vladimir, Logic programs with intensional functions, (Principles of Knowledge Representation and Reasoning: Proceedings of the Thirteenth International Conference, KR 2012, Rome, Italy, June 10-14, 2012, (2012), Springer) · Zbl 1281.68067
[29] Lin, Fangzhen; Shoham, Yoav, A logic of knowledge and justified assumptions, Artif. Intell., 57, 2-3, 271-289, (1992) · Zbl 0763.68060
[30] Lin, Fangzhen; Zhao, Yuting, ASSAT: computing answer sets of a logic program by SAT solvers, Artif. Intell., 157, 1-2, 115-137, (2004) · Zbl 1085.68544
[31] Lin, Fangzhen; Zhou, Yi, From answer set logic programming to circumscription via logic of GK, Artif. Intell., 175, 1, 264-277, (2011) · Zbl 1216.68270
[32] Maier, David; Ullman, Jeffrey D.; Vardi, Moshe Y., On the foundations of the universal relation model, ACM Trans. Database Syst., 9, 2, 283-308, (1984) · Zbl 0563.68077
[33] Marek, Victor W.; Truszczynski, Miroslaw, Stable models and an alternative logic programming paradigm, (The Logic Programming Paradigm: A 25-Year Perspective, (1999), Springer-Verlag), 375-398 · Zbl 0979.68524
[34] Niemelä, Ilkka, Logic programs with stable model semantics as a constraint programming paradigm, Ann. Math. Artif. Intell., 25, 3-4, 241-273, (1999) · Zbl 0940.68018
[35] Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare, Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-logemann-loveland procedure to \(\text{DPLL}(t)\), J. ACM, 53, 6, 937-977, (1999) · Zbl 1326.68164
[36] Pearce, David; Valverde, Agustín, Towards a first order equilibrium logic for nonmonotonic reasoning, (JELIA’2004, (2004)), 147-160 · Zbl 1111.68687
[37] Reiter, Raymond, A logic for default reasoning, Artif. Intell., 13, 1-2, 81-132, (1980) · Zbl 0435.68069
[38] Shen, Yi-Dong; Wang, Kewen; Eiter, Thomas; Fink, Michael; Redl, Christoph; Krennwallner, Thomas; Deng, Jun, FLP answer set semantics without circular justifications for general logic programs, Artif. Intell., 213, 1-41, (2014) · Zbl 1391.68016
[39] Zhang, Heng; Zhang, Yan, First-order expressibility and boundedness of disjunctive logic programs, (IJCAI 2013, (2013))
[40] Zhang, Yan; Zhou, Yi, On the progression semantics and boundedness of answer set programs, (KR 2010, (2010))
[41] Zhou, Yi, First-order disjunctive logic programming vs normal logic programming, (Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, (2015)), 3292-3298
[42] Zhou, Yi; Zhang, Yan, Progression semantics for disjunctive logic programs, (AAAI 2011, (2011))
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.