zbMATH — the first resource for mathematics

On abstract modular inference systems and solvers. (English) Zbl 1357.68230
Summary: Integrating diverse formalisms into modular knowledge representation systems offers increased expressivity, modeling convenience, and computational benefits. We introduce the concepts of abstract inference modules and abstract modular inference systems to study general principles behind the design and analysis of model generating programs, or solvers, for integrated multi-logic systems. We show how modules and modular systems give rise to transition graphs, which are a natural and convenient representation of solvers, an idea pioneered by the SAT community. These graphs lend themselves well to extensions that capture such important solver design features as learning. In the paper, we consider two flavors of learning for modular formalisms, local and global. We illustrate our approach by showing how it applies to answer set programming, propositional logic, multi-logic systems based on these two formalisms and, more generally, to satisfiability modulo theories.

68T30 Knowledge representation
68N17 Logic programming
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T27 Logic in artificial intelligence
Chaff; Clingcon; DMCS; Smodels
Full Text: DOI
[1] Apt, K.; Blair, H.; Walker, A., Towards a theory of declarative knowledge, (Minker, J., Foundations of Deductive Databases and Logic Programming, (1988), Morgan Kaufmann), 89-142
[2] Balduccini, M., Representing constraint satisfaction problems in answer set programming, (Proceedings of ICLP Workshop on Answer Set Programming and Other Computing Paradigms, ASPOCP, (2009)) · Zbl 1219.68083
[3] Barrett, C.; Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Splitting on demand in sat modulo theories, (Hermann, M.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science, vol. 4246, (2006), Springer Berlin), 512-526 · Zbl 1165.68480
[4] Barrett, C.; Sebastiani, R.; Seshia, S.; Tinelli, C., Satisfiability modulo theories, (Biere, A.; Heule, M.; van Maaren, H.; Walsh, T., Handbook of Satisfiability, (2008), IOS Press), 737-797
[5] Brain, M., An algebra of search spaces, (Frisch, A. M.; O’Sullivan, B., Proceedings of the ERCIM Workshop on Constraint Solving and Constraint Logic Programming, (2011)), 72-86
[6] Brewka, G.; Eiter, T., Equilibria in heterogeneous nonmonotonic multi-context systems, (Proceedings of the 22nd National Conference on Artificial Intelligence, AAAI 2007, (2007), AAAI Press), 385-390
[7] Brochenin, R.; Lierler, Y.; Maratea, M., Abstract disjunctive answer set solvers, (Schaub, T.; Friedrich, G.; O’Sullivan, B., Proceedings of the 21st European Conference on Artificial Intelligence, ECAI 2014, Frontiers in Artificial Intelligence and Applications, vol. 263, (2014), IOS Press), 165-170 · Zbl 1366.68016
[8] Calimeri, F.; Faber, W.; Pfeifer, G.; Leone, N., Pruning operators for disjunctive logic programming systems, Fundam. Inform., 71, 2-3, 183-214, (2006) · Zbl 1095.68114
[9] Dao-Tran, M.; Eiter, T.; Fink, M.; Krennwallner, T., Modular nonmonotonic logic programming revisited, (Hill, P.; Warren, D., Logic Programming, Lecture Notes in Computer Science, vol. 5649, (2009), Springer Berlin), 145-159 · Zbl 1251.68056
[10] de Moura, L. M.; Bjørner, N., Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77, (2011)
[11] Denecker, M.; Lierler, Y.; Truszczynski, M.; Vennekens, J., A Tarskian informal semantics for answer set programming, (Dovier, A.; Costa, V. S., ICLP (Technical Communications), LIPIcs, vol. 17, (2012), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 277-289 · Zbl 1281.68147
[12] D’Silva, V.; Haller, L.; Kroening, D., Abstract conflict driven learning, (Giacobazzi, R.; Cousot, R., The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, (2013), ACM), 143-154 · Zbl 1301.68156
[13] East, D.; Truszczynski, M., Predicate-calculus-based logics for modeling and solving search problems, ACM Trans. Comput. Log., 7, 1, 38-83, (2006) · Zbl 1367.68264
[14] Eiter, T.; Fink, M.; Krennwallner, T.; Redl, C., Conflict-driven ASP solving with external sources, Theory Pract. Log. Program., 12, 4-5, 659-679, (Sep. 2012)
[15] Eiter, T.; Ianni, G.; Schindlauer, R.; Tompits, H., A uniform integration of higher-order reasoning and external evaluations in answer-set programming, (Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI 2005, (2005), Morgan Kaufmann San Francisco, CA, USA), 90-96
[16] El-Din Bairakdar, S.; Dao-Tran, M.; Eiter, T.; Fink, M.; Krennwallner, T., The DMCS solver for distributed nonmonotonic multi-context systems, (Janhunen, T.; Niemelä, I., Proceedings of the 12th European Conference on Logics in Artificial Intelligence, JELIA 2010, LNCS, vol. 6341, (2010), Springer Berlin), 352-355 · Zbl 1306.68201
[17] Gebser, M.; Kaufmann, B.; Neumann, A.; Schaub, T., Conflict-driven answer set solving, (Proceedings of the 20th International Joint Conference on Artificial Intelligence, IJCAI 2007, (2007), Morgan Kaufmann San Francisco, CA, USA), 386-392
[18] Gebser, M.; Kaufmann, B.; Schaub, T., Solution enumeration for projected Boolean search problems, (van Hoeve, W.-J.; Hooker, J., Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, Lecture Notes in Computer Science, vol. 5547, (2009), Springer Berlin), 71-86 · Zbl 1241.68100
[19] Gebser, M.; Kaufmann, B.; Schaub, T., Conflict-driven answer set solving: from theory to practice, Artif. Intell., 187, 52-89, (2012) · Zbl 1251.68060
[20] Gebser, M.; Ostrowski, M.; Schaub, T., Constraint answer set solving, (Proceedings of 25th International Conference on Logic Programming, ICLP, (2009), Springer Berlin), 235-249 · Zbl 1251.68061
[21] Gebser, M.; Schaub, T., Tableau calculi for answer set programming, (Etalle, S.; Truszczynski, M., Proceedings of the 22nd International Conference on Logic Programming, ICLP 2006, LNCS, vol. 4079, (2006), Springer Berlin), 11-25 · Zbl 1131.68375
[22] Gelfond, M.; Lifschitz, V., The stable model semantics for logic programming, (Kowalski, R.; Bowen, K., Proceedings of International Logic Programming Conference and Symposium, (1988), MIT Press), 1070-1080
[23] Gelfond, M.; Lifschitz, V., Classical negation in logic programs and disjunctive databases, New Gener. Comput., 9, 365-385, (1991) · Zbl 0735.68012
[24] Giunchiglia, E.; Leone, N.; Maratea, M., On the relation among answer set solvers, Ann. Math. Artif. Intell., 53, 1-4, 169-204, (2008) · Zbl 1165.68333
[25] Giunchiglia, E.; Lierler, Y.; Maratea, M., Answer set programming based on propositional satisfiability, J. Autom. Reason., 36, 345-377, (2006) · Zbl 1107.68029
[26] Gomes, C. P.; Kautz, H.; Sabharwal, A.; Selman, B., Satisfiability solvers, (van Harmelen, F.; Lifschitz, V.; Porter, B., Handbook of Knowledge Representation, (2008), Elsevier), 89-134
[27] Gomes, C. P.; Sabharwal, A.; Selman, B., Model counting, (Handbook of Satisfiability, (2009), IOS Press), 633-654
[28] Jaffar, J.; Lassez, J., Constraint logic programming, (Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, Munich, Germany, January 21-23, 1987, (1987), ACM Press), 111-119
[29] Jaffar, J.; Maher, M., Constraint logic programming: a survey, J. Log. Program., 19, 20, 503-581, (1994)
[30] Janhunen, T., Modular equivalence in general, (19th European Conference on Artificial Intelligence, ECAI, (2008)), 75-79
[31] Janhunen, T.; Liu, G.; Niemelä, I., 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))
[32] Janhunen, T.; Oikarinen, E.; Tompits, H.; Woltran, S., Modularity aspects of disjunctive stable models, (Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR’07, (2007), Springer Berlin), 175-187 · Zbl 1149.68334
[33] Järvisalo, M.; Oikarinen, E.; Janhunen, T.; Niemelä, I., A module-based framework for multi-language constraint modeling, (Erdem, E.; Lin, F.; Schaub, T., Proceedings of the 10th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2009, LNCS, vol. 5753, (2009), Springer Berlin), 155-168 · Zbl 1258.68136
[34] Lierler, Y., Abstract answer set solvers with backjumping and learning, Theory Pract. Log. Program., 11, 135-169, (2011) · Zbl 1220.68038
[35] Lierler, Y., Relating constraint answer set programming languages and algorithms, Artif. Intell., 207, 1-22, (2014) · Zbl 1334.68041
[36] Lierler, Y.; Truszczynski, M., Transition systems for model generators — a unifying approach, 27th International Conference on Logic Programming, ICLP 2011, Theory Pract. Log. Program., 11, 4-5, (2011), Special Issue
[37] Lierler, Y.; Truszczynski, M., Modular answer set solving, (Late-Breaking Developments in the Field of Artificial Intelligence, AAAI Workshops, vol. WS-13-17, (2013), AAAI)
[38] Lierler, Y.; Truszczynski, M., Abstract modular inference systems and solvers, (Flatt, M.; Guo, H.-F., Practical Aspects of Declarative Languages, Lecture Notes in Computer Science, vol. 8324, (2014), Springer Berlin), 49-64
[39] Lierler, Y.; Truszczynski, M., An abstract view on modularity in knowledge representation, (Bonet, B.; Koenig, S., Proceedings of the 29th AAAI Conference on Artificial Intelligence, (2015)), 1532-1538
[40] Lifschitz, V.; Pearce, D.; Valverde, A., Strongly equivalent logic programs, ACM Trans. Comput. Log., 2, 4, 526-541, (2001) · Zbl 1365.68149
[41] Lifschitz, V.; Turner, H., Splitting a logic program, (Hentenryck, P. V., Proceedings of the 11th International Conference on Logic Programming, ICLP 1994, (1994)), 23-37
[42] Marek, V.; Truszczyński, M., Stable models and an alternative logic programming paradigm, (The Logic Programming Paradigm: a 25-Year Perspective, (1999), Springer Berlin), 375-398 · Zbl 0979.68524
[43] Mariën, M.; Wittocx, J.; Denecker, M.; Bruynooghe, M., SAT(ID): satisfiability of propositional logic extended with inductive definitions, (Büning, H. K.; Zhao, X., Proceedings of the 11th International Conference on Theory and Applications of Satisfiability Testing, SAT 2008, LNCS, vol. 4996, (2008), Springer Berlin), 211-224 · Zbl 1138.68547
[44] Marques Silva, J. P.; Lynce, I.; Malik, S., Conflict-driven clause learning SAT solvers, (Handbook of Satisfiability, (2009), IOS Press), 131-153
[45] Mellarkod, V. S.; Gelfond, M.; Zhang, Y., Integrating answer set programming and constraint logic programming, Ann. Math. Artif. Intell., 53, 1-4, 251-287, (2008) · Zbl 1165.68504
[46] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient SAT solver, (Proceedings DAC-01, (2001))
[47] Niemelä, I., Logic programs with stable model semantics as a constraint programming paradigm, Ann. Math. Artif. Intell., 25, 241-273, (1999) · Zbl 0940.68018
[48] Niemelä, I.; Simons, P., Extending the smodels system with cardinality and weight constraints, (Minker, J., Logic-Based Artificial Intelligence, (2000), Kluwer), 491-521 · Zbl 0979.68015
[49] Nieuwenhuis, R.; Oliveras, A.; Tinelli, C., Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-logemann-loveland procedure to DPLL(T), J. ACM, 53, 6, 937-977, (2006) · Zbl 1326.68164
[50] Oikarinen, E.; Janhunen, T., Modular equivalence for normal logic programs, (Brewka, G.; Coradeschi, S.; Perini, A.; Traverso, P., Proceedings of the 17th European Conference on Artificial Intelligence, ECAI 2006, (2006), IOS Press Amsterdam, The Netherlands), 412-416
[51] Rossi, F.; van Beek, P.; Walsh, T., Constraint programming, (van Harmelen, F.; Lifschitz, V.; Porter, B., Handbook of Knowledge Representation, (2008), Elsevier), 181-212
[52] Saccà, D.; Zaniolo, C., Stable models and non-determinism in logic programs with negation, (Rosenkrantz, D. J.; Sagiv, Y., Proceedings of the 9th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, PODS 1990, (1990), ACM New York, NY, USA), 205-217
[53] Simons, P.; Niemelä, I.; Soininen, T., Extending and implementing the stable model semantics, Artif. Intell., 138, 181-234, (2002) · Zbl 0995.68021
[54] Tasharrofi, S.; Ternovska, E., A semantic account for modularity in multi-language modelling of search problems, (Tinelli, C.; Sofronie-Stokkermans, V., Proceedings of the 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011, LNCS, vol. 6989, (2011), Springer Berlin), 259-274 · Zbl 1348.68232
[55] Tasharrofi, S.; Wu, X. N.; Ternovska, E., Solving modular model expansion tasks, (2011), CoRR
[56] Van Gelder, A.; Ross, K.; Schlipf, J., The well-founded semantics for general logic programs, J. ACM, 38, 3, 620-650, (1991) · Zbl 0799.68045
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.