Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016), ICLP 2016 TCs, October 16-21, 2016, New York City, USA
ICLP 2016 TCs
October 16-21, 2016
New York City, USA
International Conference on Logic Programming
ICLP
https://www.cs.nmsu.edu/ALP/conferences/
https://dblp.org/db/conf/iclp
Open Access Series in Informatics
OASIcs
https://www.dagstuhl.de/dagpub/2190-6807
https://dblp.org/db/series/oasics
2190-6807
Manuel
Carro
Manuel Carro
Andy
King
Andy King
Neda
Saeedloei
Neda Saeedloei
Marina
De Vos
Marina De Vos
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
52
2016
978-3-95977-007-1
https://www.dagstuhl.de/dagpub/978-3-95977-007-1
Front Matter, Table of Contents, Preface, List of Authors
Front Matter, Table of Contents, Preface, List of Authors
Front Matter
Table of Contents
Preface
List of Authors
0:i-0:xvi
Front Matter
Manuel
Carro
Manuel Carro
Andy
King
Andy King
Neda
Saeedloei
Neda Saeedloei
Marina
De Vos
Marina De Vos
10.4230/OASIcs.ICLP.2016.0
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
SMT-Based Constraint Answer Set Solver EZSMT (System Description)
Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. Recently, the formal link between this research area and satisfiability modulo theories (or SMT) was established. This link allows the cross-fertilization between traditionally different solving technologies. The paper presents the system ezsmt, one of the first SMT-based solvers for constraint answer set programming. It also presents the comparative analysis of the performance of ezsmt in relation to its peers including solvers EZCSP, CLINGCON, and MINGO. Experimental results demonstrate that SMT is a viable technology for constraint answer set programming.
constraint answer set programming
constraint satisfaction processing
satisfiability modulo theories
1:1-1:15
System Description
Benjamin
Susman
Benjamin Susman
Yuliya
Lierler
Yuliya Lierler
10.4230/OASIcs.ICLP.2016.1
Marcello Balduccini. Representing constraint satisfaction problems in answer set programming. In ICLP Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP), 2009. URL: https://www.mat.unical.it/ASPOCP09/.
https://www.mat.unical.it/ASPOCP09/
Marcello Balduccini and Yuliya Lierler. Constraint answer set solver EZCSP and why integration schemas matter. Unpublished draft, available at https://works.bepress.com/yuliya_lierler/64/, 2016.
https://works.bepress.com/yuliya_lierler/64/
Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. Cvc4. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV'11), volume 6806 of LNCS. Springer, 2011.
Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.5. Technical report, Department of Computer Science, The University of Iowa, 2015.
Michael Bartholomew and Joohyung Lee. System aspmt2smt: Computing aspmt theories by smt solvers. In European Conference on Logics in Artificial Intelligence, JELIA, pages 529-542. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11558-0_37.
http://dx.doi.org/10.1007/978-3-319-11558-0_37
Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340, 2008.
Christian Drescher and Toby Walsh. A translational approach to constraint answer set solving. Theory and Practice of Logic programming (TPLP), 10(4-6):465-480, 2010.
François Fages. Consistency of Clark’s completion and existence of stable models. Journal of Methods of Logic in Computer Science, 1:51-60, 1994.
Paolo Ferraris and Vladimir Lifschitz. Weight constraints as nested expressions. Theory and Practice of Logic Programming, 5:45-74, 2005.
Martin Gebser, Roland Kaminski, Arne König, and Torsten Schaub. Advances in gringo series 3. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pages 345-351. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-20895-9_39.
http://dx.doi.org/10.1007/978-3-642-20895-9_39
Martin Gebser, Max Ostrowski, and Torsten Schaub. Constraint answer set solving. In Proceedings of 25th International Conference on Logic Programming, pages 235-249. Springer, 2009.
Enrico Giunchiglia, Yuliya Lierler, and Marco Maratea. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning, 36:345-377, 2006.
Tomi Janhunen, Guohua Liu, and Ilkka Niemela. Tight integration of non-ground answer set programming and satisfiability modulo theories. In Proceedings of the 1st Workshop on Grounding and Transformations for Theories with Variables, 2011.
Yuliya Lierler and Benjamin Susman. Constraint answer set programming versus satisfiability modulo theories. In Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI), 2016.
Vladimir Lifschitz, Lappoon R. Tang, and Hudson Turner. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25:369-389, 1999.
Guohua Liu, Tomi Janhunen, and Ilkka Niemela. Answer set programming via mixed integer programming. In Knowledge Representation and Reasoning Conference, 2012. URL: https://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4516.
https://www.aaai.org/ocs/index.php/KR/KR12/paper/view/4516
Kim Marriott and Peter J. Stuckey. Programming with Constraints: An Introduction. MIT Press, 1998.
Ilkka Niemelä. Stable models and difference logic. Annals of Mathematics and Artificial Intelligence, 53:313-329, 2008.
Ilkka Niemelä and Patrik Simons. Extending the Smodels system with cardinality and weight constraints. In Jack Minker, editor, Logic-Based Artificial Intelligence, pages 491-521. Kluwer, 2000.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Theory Solving Made Easy with Clingo 5
Answer Set Programming (ASP) is a model, ground, and solve paradigm. The integration of application- or theory-specific reasoning into ASP systems thus impacts on many if not all elements of its workflow, viz. input language, grounding, intermediate language, solving, and output format. We address this challenge with the fifth generation of the ASP system clingo and its grounding and solving components by equipping them with well-defined generic interfaces facilitating the manifold integration efforts. On the grounder's side, we introduce a generic way of specifying language extensions and propose an intermediate format accommodating their ground representation. At the solver end, this is accompanied by high-level interfaces easing the integration of theory propagators dealing with these extensions.
Answer Set Programming
Theory Language
Theory Propagation
2:1-2:15
Regular Paper
Martin
Gebser
Martin Gebser
Roland
Kaminski
Roland Kaminski
Benjamin
Kaufmann
Benjamin Kaufmann
Max
Ostrowski
Max Ostrowski
Torsten
Schaub
Torsten Schaub
Philipp
Wanko
Philipp Wanko
10.4230/OASIcs.ICLP.2016.2
M. Abseher, B. Bliem, G. Charwat, F. Dusberger, M. Hecher, and S. Woltran. The D-FLAT system for dynamic programming on tree decompositions. In Fermé and Leite [15], pages 558-572.
M. Balduccini. Representing constraint satisfaction problems in answer set programming. In Proceedings of the Second Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP'09), pages 16-30, 2009.
M. Banbara, B. Kaufmann, M. Ostrowski, and T. Schaub. Clingcon: The next generation. Submitted for publication, 2016.
C. Barrett, R. Sebastiani, S. Seshia, and C. Tinelli. Satisfiability modulo theories. In Biere et al. [7], pages 825-885.
M. Bartholomew and J. Lee. System aspmt2smt: Computing ASPMT theories by SMT solvers. In Fermé and Leite [15], pages 529-542.
R. Bellman. On a routing problem. Quarterly of Applied Mathematics, 16:87-90, 1958.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability. IOS Press, 2009.
J. Bomanson, M. Gebser, T. Janhunen, B. Kaufmann, and T. Schaub. Answer set programming modulo acyclicity. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), pages 143-150. Springer, 2015.
P. Cabalar, R. Kaminski, M. Ostrowski, and T. Schaub. An ASP semantics for default reasoning with constraints. In Proceedings of the Twenty-fifth International Joint Conference on Artificial Intelligence (IJCAI'16), pages 1015-1021. IJCAI/AAAI Press, 2016.
F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, F. Ricca, and T. Schaub. ASP-Core-2: Input language format. Available at https://www.mat.unical.it/aspcomp2013/ASPStandardization/, 2012.
https://www.mat.unical.it/aspcomp2013/ASPStandardization/
S. Cotton and O. Maler. Fast and flexible difference constraint propagation for DPLL(T). In Proceedings of the Ninth International Conference on Theory and Applications of Satisfiability Testing (SAT'06), pages 170-183. Springer, 2006.
C. Drescher and T. Walsh. Answer set solving with lazy nogood generation. In Technical Communications of the Twenty-eighth International Conference on Logic Programming (ICLP'12), pages 188-200. Leibniz International Proceedings in Informatics, 2012.
T. Eiter, E. Erdem, H. Erdogan, and M. Fink. Finding similar/diverse solutions in answer set programming. Theory and Practice of Logic Programming, 13(3):303-359, 2013.
T. Eiter, M. Fink, T. Krennwallner, and C. Redl. Conflict-driven ASP solving with external sources. Theory and Practice of Logic Programming, 12(4-5):659-679, 2012.
E. Fermé and J. Leite, editors. Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA'14), volume 8761 of Lecture Notes in Artificial Intelligence. Springer, 2014.
L. Ford and D. Fulkerson. Flows in networks. Princeton University Press, 1962.
M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, and P. Wanko. Theory solving made easy with clingo 5 (extended version). Available at http://www.cs.uni-potsdam.de/wv/publications/, 2016.
http://www.cs.uni-potsdam.de/wv/publications/
M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Clingo = ASP + control: Preliminary report. In Technical Communications of the Thirtieth International Conference on Logic Programming (ICLP'14), 2014. Available at URL: http://arxiv.org/abs/1405.3694.
http://arxiv.org/abs/1405.3694
M. Gebser, B. Kaufmann, R. Otero, J. Romero, T. Schaub, and P. Wanko. Domain-specific heuristics in answer set programming. In Proceedings of the Twenty-Seventh National Conference on Artificial Intelligence (AAAI'13), pages 350-356. AAAI Press, 2013.
M. Gebser, B. Kaufmann, and T. Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012.
T. Janhunen, G. Liu, and I. Niemelä. Tight integration of non-ground answer set programming and satisfiability modulo theories. In Proceedings of the First Workshop on Grounding and Transformation for Theories with Variables (GTTV'11), pages 1-13, 2011.
V. Lifschitz. What is answer set programming? In Proceedings of the Twenty-third National Conference on Artificial Intelligence (AAAI'08), pages 1594-1597. AAAI Press, 2008.
G. Liu, T. Janhunen, and I. Niemelä. Answer set programming via mixed integer programming. In Proceedings of the Thirteenth International Conference on Principles of Knowledge Representation and Reasoning (KR'12), pages 32-42. AAAI Press, 2012.
J. Marques-Silva, I. Lynce, and S. Malik. Conflict-driven clause learning SAT solvers. In Biere et al. [7], pages 131-153.
M. Ostrowski and T. Schaub. ASP modulo CSP: The clingcon system. Theory and Practice of Logic Programming, 12(4-5):485-503, 2012.
P. Simons, I. Niemelä, and T. Soininen. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2):181-234, 2002.
E. Taillard. Benchmarks for basic scheduling problems. European Journal of Operational Research, 64(2):278-285, 1993.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Computing Diverse Optimal Stable Models
We introduce a comprehensive framework for computing diverse (or similar) solutions to logic programs with preferences. Our framework provides a wide spectrum of complete and incomplete methods for solving this task. Apart from proposing several new methods, it also accommodates existing ones and generalizes them to programs with preferences. Interestingly, this is accomplished by integrating and automating several basic ASP techniques - being of general interest even beyond diversification. The enabling factor of this lies in the recent advance of multi-shot ASP solving that provides us with fine-grained control over reasoning processes and abolishes the need for solver modifications and wrappers that were indispensable in previous approaches. Our framework is implemented as an extension to the ASP-based preference handling system asprin. We use the resulting system asprin 2 for an empirical evaluation of the diversification methods comprised in our framework.
Answer Set Programming
Diversity
Similarity
Preferences
3:1-3:14
Regular Paper
Javier
Romero
Javier Romero
Torsten
Schaub
Torsten Schaub
Philipp
Wanko
Philipp Wanko
10.4230/OASIcs.ICLP.2016.3
asprin. URL: http://www.cs.uni-potsdam.de/asprin.
http://www.cs.uni-potsdam.de/asprin
Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13). Springer, 2013.
B. Andres, M. Gebser, M. Glaß, C. Haubelt, F. Reimann, and T. Schaub. Symbolic system synthesis using answer set programming. In Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13) [2], pages 79-91.
M. Banbara, T. Soh, N. Tamura, K. Inoue, and T. Schaub. Answer set programming as a modeling language for course timetabling. Theory and Practice of Logic Programming, 13(4-5):783-798, 2013.
C. Baral. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, 2003.
G. Brewka, J. Delgrande, J. Romero, and T. Schaub. asprin: Customizing answer set preferences without a headache. In Proceedings of the Twenty-Ninth National Conference on Artificial Intelligence (AAAI'15), pages 1467-1474. AAAI Press, 2015.
G. Brewka, J. Delgrande, J. Romero, and T. Schaub. Implementing preferences with asprin. In Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), pages 158-172. Springer, 2015.
G. Brewka, I. Niemelä, and M. Truszczyński. Answer set optimization. In Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence (IJCAI'03), pages 867-872. Morgan Kaufmann, 2003.
T. Eiter, E. Erdem, H. Erdogan, and M. Fink. Finding similar/diverse solutions in answer set programming. Theory and Practice of Logic Programming, 13(3):303-359, 2013.
T. Eiter and G. Gottlob. On the computational cost of disjunctive logic programming. Annals of Mathematics and Artificial Intelligence, 15(3-4):289-323, 1995.
T. Eiter and A. Polleres. Towards automated integration of guess and check programs in answer set programming: a meta-interpreter and applications. Theory and Practice of Logic Programming, 6(1-2):23-60, 2006.
M. Gebser, C. Guziolowski, M. Ivanchev, T. Schaub, A. Siegel, S. Thiele, and P. Veber. Repair and prediction (under inconsistency) in large biological networks with answer set programming. In Proceedings of the Twelfth International Conference on Principles of Knowledge Representation and Reasoning (KR'10), pages 497-507. AAAI Press, 2010.
M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub. Clingo = ASP + control: Preliminary report. In Technical Communications of the Thirtieth International Conference on Logic Programming (ICLP'14), volume 14 of Theory and Practice of Logic Programming, 2014.
M. Gebser, R. Kaminski, and T. Schaub. Complex optimization in answer set programming. Theory and Practice of Logic Programming, 11(4-5):821-839, 2011.
M. Gebser, B. Kaufmann, R. Otero, J. Romero, T. Schaub, and P. Wanko. Domain-specific heuristics in answer set programming. In Proceedings of the Twenty-Seventh National Conference on Artificial Intelligence (AAAI'13), pages 350-356. AAAI Press, 2013.
M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Computing, 9:365-385, 1991.
E. Hebrard, B. Hnich, B. O'Sullivan, and T. Walsh. Finding diverse and similar solutions in constraint programming. In Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI'05), pages 372-377. AAAI Press, 2005.
A. Nadel. Generating diverse solutions in SAT. In Proceedings of the Fourteenth International Conference on Theory and Applications of Satisfiability Testing (SAT'11), pages 287-301. Springer, 2011.
V. Pareto. Cours d'economie politique. Librairie Droz, 1964.
J. Romero, T. Schaub, and P. Wanko. Computing diverse optimal stable models (extended version). Available at http://www.cs.uni-potsdam.de/wv/publications/, 2016.
http://www.cs.uni-potsdam.de/wv/publications/
T. Schaub and S. Thiele. Metabolic network expansion with ASP. In Proceedings of the Twenty-fifth International Conference on Logic Programming (ICLP'09), pages 312-326. Springer, 2009.
H. Shimazu. Expertclerk: Navigating shoppers' buying process with the combination of asking and proposing. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI'01), pages 1443-1448. Morgan Kaufmann, 2001.
S. Siddiqi. Computing minimum-cardinality diagnoses by model relaxation. In Proceedings of the Twenty-second International Joint Conference on Artificial Intelligence (IJCAI'11), pages 1087-1092. IJCAI/AAAI Press, 2011.
P. Simons, I. Niemelä, and T. Soininen. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2):181-234, 2002.
Y. Zhu and M. Truszczyński. On optimal solutions of answer set optimization problems. In Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13) [2], pages 556-568.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Answer Set Programming for Qualitative Spatio-Temporal Reasoning: Methods and Experiments
We study the translation of reasoning problems involving qualitative spatio-temporal calculi into answer set programming (ASP). We present various alternative transformations and provide a qualitative comparison among them. An implementation of these transformations is provided by a tool that transforms problem instances specified in the language of the Generic Qualitative Reasoner (GQR) into ASP problems. Finally, we report on an experimental analysis of solving consistency problems for Allen's Interval Algebra and the Region Connection Calculus with eight base relations (RCC-8).
answer set programming
qualitative spatio-temporal reasoning
4:1-4:15
Regular Paper
Christopher
Brenton
Christopher Brenton
Wolfgang
Faber
Wolfgang Faber
Sotiris
Batsakis
Sotiris Batsakis
10.4230/OASIcs.ICLP.2016.4
James F. Allen. An interval-based representation of temporal knowledge. In Patrick J. Hayes, editor, Proceedings of the 7th International Joint Conference on Artificial Intelligence (IJCAI'81), Vancouver, BC, Canada, August 1981, pages 221-226. William Kaufmann, 1981.
Chitta Baral. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, 2003.
Robert Battle and Dave Kolas. Enabling the geospatial semantic web with parliament and geosparql. Semantic Web, 3(4):355-370, 2012.
Christopher Brenton, Wolfgang Faber, and Sotiris Batsakis. Solving qualitative spatio-temporal reasoning problems by means of answer set programming: Methods and experiments. In Proceedings of the Eighth Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP 2015), Cork, Ireland, 2015.
Gerhard Brewka, James P. Delgrande, Javier Romero, and Torsten Schaub. Implementing preferences with asprin. In Francesco Calimeri, Giovambattista Ianni, and Miroslaw Truszczynski, editors, Logic Programming and Nonmonotonic Reasoning - 13th International Conference (LPNMR 2015), volume 9345 of Lecture Notes in Computer Science, pages 158-172. Springer, 2015.
Anthony G. Cohn, Brandon Bennett, John Gooday, and Nicholas Mark Gotts. Qualitative spatial representation and reasoning with the region connection calculus. GeoInformatica, 1(3):275-316, 1997.
Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub. Answer Set Solving in Practice. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan and Claypool Publishers, 2012.
Michael Gelfond and Vladimir Lifschitz. The Stable Model Semantics for Logic Programming. In Logic Programming: Proceedings Fifth Intl Conference and Symposium, pages 1070-1080, Cambridge, Mass., 1988. MIT Press.
Jason Jingshi Li. Qualitative spatial and temporal reasoning with answer set programming. In IEEE 24th International Conference on Tools with Artificial Intelligence, ICTAI 2012, pages 603-609, 2012.
Till Mossakowski and Reinhard Moratz. Qualitative reasoning about relative direction of oriented points. Artificial Intelligence, 180-181:34-45, 2012.
Jochen Renz and Bernhard Nebel. Efficient methods for qualitative spatial reasoning. Journal of Artificial Intelligence Research, 15:289-318, 2001.
Jochen Renz and Bernhard Nebel. Qualitative spatial reasoning using constraint calculi. In Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors, Handbook of Spatial Logics, pages 161-215. Springer, 2007.
Przemysław Andrzej Wałega, Mehul Bhatt, and Carl P. L. Schultz. ASPMT(QS): non-monotonic spatial reasoning with answer set programming modulo theories. In Francesco Calimeri, Giovambattista Ianni, and Mirosław Truszczyński, editors, Logic Programming and Nonmonotonic Reasoning - 13th International Conference (LPNMR 2015), volume 9345 of Lecture Notes in Computer Science, pages 488-501. Springer, 2015.
Matthias Westphal, Stefan Wölfl, and Zeno Gantner. GQR: a fast solver for binary qualitative constraint networks. In Benchmarking of Qualitative Spatial and Temporal Reasoning Systems, Papers from the 2009 AAAI Spring Symposium, Technical Report SS-09-02, Stanford, California, USA, March 23-25, 2009, pages 51-52, 2009.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Rewriting Optimization Statements in Answer-Set Programs
Constraints on Pseudo-Boolean (PB) expressions can be translated into Conjunctive Normal Form (CNF) using several known translations. In Answer-Set Programming (ASP), analogous expressions appear in weight rules and optimization statements. Previously, we have translated weight rules into normal rules, using normalizations designed in accord with existing CNF encodings. In this work, we rededicate such designs to rewrite optimization statements in ASP. In this context, a rewrite of an optimization statement is a replacement accompanied by a set of normal rules that together replicate the original meaning. The goal is partially the same as in translating PB constraints or weight rules: to introduce new meaningful auxiliary atoms that may help a solver in the search for (optimal) solutions. In addition to adapting previous translations, we present selective rewriting techniques in order to meet the above goal while using only a limited amount of new rules and atoms. We experimentally evaluate these methods in preprocessing ASP optimization statements and then searching for optimal answer sets. The results exhibit significant advances in terms of numbers of optimally solved instances, reductions in search conflicts, and shortened computation times. By appropriate choices of rewriting techniques, improvements are made on instances involving both small and large weights. In particular, we show that selective rewriting is paramount on benchmarks involving large weights.
Answer-Set Programming
Pseudo-Boolean optimization
Translation methods
5:1-5:15
Regular Paper
Jori
Bomanson
Jori Bomanson
Martin
Gebser
Martin Gebser
Tomi
Janhunen
Tomi Janhunen
10.4230/OASIcs.ICLP.2016.5
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Valentin Mayer-Eichberger. A new look at BDDs for Pseudo-Boolean constraints. Journal of Artificial Intelligence Research, 45:443-480, 2012. URL: http://dx.doi.org/10.1613/jair.3653.
http://dx.doi.org/10.1613/jair.3653
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, and Peter J. Stuckey. To encode or to propagate? The best choice for each constraint in SAT. In Proceedings of CP 2013, volume 8124 of LNCS, pages 97-106. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40627-0_10.
http://dx.doi.org/10.1007/978-3-642-40627-0_10
Ignasi Abío and Peter J. Stuckey. Conflict directed lazy decomposition. In Proceedings of CP 2012, volume 7514 of LNCS, pages 70-85. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33558-7_8.
http://dx.doi.org/10.1007/978-3-642-33558-7_8
Mario Alviano, Carmine Dodaro, Nicola Leone, and Francesco Ricca. Advances in WASP. In Calimeri et al. [16], pages 40-54. URL: http://dx.doi.org/10.1007/978-3-319-23264-5_5.
http://dx.doi.org/10.1007/978-3-319-23264-5_5
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez-Carbonell. Cardinality networks: A theoretical and empirical study. Constraints, 16(2):195-221, 2011. URL: http://dx.doi.org/10.1007/s10601-010-9105-0.
http://dx.doi.org/10.1007/s10601-010-9105-0
Olivier Bailleux, Yacine Boufkhad, and Olivier Roussel. New encodings of Pseudo-Boolean constraints into CNF. In Proceedings of SAT 2009, volume 5584 of LNCS, pages 181-194. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02777-2_19.
http://dx.doi.org/10.1007/978-3-642-02777-2_19
Mutsunori Banbara, Takehide Soh, Naoyuki Tamura, Katsumi Inoue, and Torsten Schaub. Answer set programming as a modeling language for course timetabling. Theory and Practice of Logic Programming, 13(4-5):783-798, 2013. URL: http://dx.doi.org/10.1017/S1471068413000495.
http://dx.doi.org/10.1017/S1471068413000495
Kenneth E. Batcher. Sorting networks and their applications. In Proceedings of AFIPS 1968, pages 307-314. ACM, 1968. URL: http://dx.doi.org/10.1145/1468075.1468121.
http://dx.doi.org/10.1145/1468075.1468121
Yael Ben-Haim, Alexander Ivrii, Oded Margalit, and Arie Matsliah. Perfect hashing and CNF encodings of cardinality constraints. In Proceedings of SAT 2012, volume 7317 of LNCS, pages 397-409. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-31612-8_30.
http://dx.doi.org/10.1007/978-3-642-31612-8_30
Jori Bomanson, Martin Gebser, and Tomi Janhunen. Improving the normalization of weight rules in answer set programs. In Proceedings of JELIA 2014, volume 8761 of LNCS, pages 166-180. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11558-0_12.
http://dx.doi.org/10.1007/978-3-319-11558-0_12
Jori Bomanson and Tomi Janhunen. Normalizing cardinality rules using merging and sorting constructions. In Proceedings of LPNMR 2013, volume 8148 of LNCS, pages 187-199. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40564-8_19.
http://dx.doi.org/10.1007/978-3-642-40564-8_19
Alex Bonutti, Fabio De Cesco, Luca Di Gaspero, and Andrea Schaerf. Benchmarking curriculum-based course timetabling: Formulations, data formats, instances, validation, visualization, and results. Annals of Operations Research, 194(1):59-70, 2012. URL: http://dx.doi.org/10.1007/s10479-010-0707-0.
http://dx.doi.org/10.1007/s10479-010-0707-0
Gerhard Brewka, Thomas Eiter, and Mirosław Truszczyński. Answer set programming at a glance. Communications of the ACM, 54(12):92-103, 2011. URL: http://dx.doi.org/10.1145/2043174.2043195.
http://dx.doi.org/10.1145/2043174.2043195
Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Francesco Ricca, and Torsten Schaub. ASP-Core-2: Input language format. Available at https://www.mat.unical.it/aspcomp2013/ASPStandardization/, 2012.
https://www.mat.unical.it/aspcomp2013/ASPStandardization/
Francesco Calimeri, Martin Gebser, Marco Maratea, and Francesco Ricca. Design and results of the fifth answer set programming competition. Artificial Intelligence, 231:151-181, 2016. URL: http://dx.doi.org/10.1016/j.artint.2015.09.008.
http://dx.doi.org/10.1016/j.artint.2015.09.008
Francesco Calimeri, Giovambattista Ianni, and Miroslaw Truszczynski, editors. Proceedings of LPNMR 2015, volume 9345 of LNCS. Springer, 2015. URL: http://dx.doi.org/10.1007/978-3-319-23264-5.
http://dx.doi.org/10.1007/978-3-319-23264-5
Broes De Cat, Bart Bogaerts, Maurice Bruynooghe, Gerda Janssens, and Marc Denecker. Predicate logic as a modelling language: The IDP system. Available at https://arxiv.org/abs/1401.6312, 2016.
https://arxiv.org/abs/1401.6312
Michael Codish, Yoav Fekete, Carsten Fuhs, and Peter Schneider-Kamp. Optimal base encodings for Pseudo-Boolean constraints. In Proceedings of TACAS 2011, volume 6605 of LNCS, pages 189-204. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-19835-9_16.
http://dx.doi.org/10.1007/978-3-642-19835-9_16
Jukka Corander, Tomi Janhunen, Jussi Rintanen, Henrik J. Nyman, and Johan Pensar. Learning chordal Markov networks by constraint satisfaction. In Proceedings of NIPS 2014, pages 1349-1357. NIPS Foundation, 2013.
James Cussens. Bayesian network learning with cutting planes. In Proceedings of UAI 2011, pages 153-160. AUAI, 2011.
Niklas Eén and Niklas Sörensson. Translating Pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, 2006.
Martin Gebser, Benjamin Kaufmann, and Torsten Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012. URL: http://dx.doi.org/10.1016/j.artint.2012.04.001.
http://dx.doi.org/10.1016/j.artint.2012.04.001
Martin Gebser, Marco Maratea, and Francesco Ricca. The design of the sixth answer set programming competition. In Calimeri et al. [16], pages 531-544. URL: http://dx.doi.org/10.1007/978-3-319-23264-5_44.
http://dx.doi.org/10.1007/978-3-319-23264-5_44
Tommi S. Jaakkola, David A. Sontag, Amir Globerson, and Marina Meila. Learning Bayesian network structure using LP relaxations. In Proceedings of AISTATS 2010, pages 358-365. JMLR Proceedings, 2010.
Tomi Janhunen, Martin Gebser, Jussi Rintanen, Henrik J. Nyman, Johan Pensar, and Jukka Corander. Learning discrete decomposable graphical models via constraint optimization. Statistics and Computing, online access, 2015. URL: http://dx.doi.org/10.1007/s11222-015-9611-4.
http://dx.doi.org/10.1007/s11222-015-9611-4
Tomi Janhunen and Ilkka Niemelä. Applying visible strong equivalence in answer-set program transformations. In Essays on Logic-Based AI in Honour of Vladimir Lifschitz, volume 7265 of LNCS, pages 363-379. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-30743-0_24.
http://dx.doi.org/10.1007/978-3-642-30743-0_24
Nicola Leone, Gerald Pfeifer, Wolfgang Faber, Thomas Eiter, Georg Gottlob, Simona Perri, and Francesco Scarcello. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic, 7(3):499-562, 2006. URL: http://dx.doi.org/10.1145/1149114.1149117.
http://dx.doi.org/10.1145/1149114.1149117
Panagiotis Manolios and Vasilis Papavasileiou. Pseudo-Boolean solving by incremental translation to SAT. In Proceedings of FMCAD 2011, pages 41-45. FMCAD Inc., 2011.
Norbert Manthey, Tobias Philipp, and Peter Steinke. A more compact translation of Pseudo-Boolean constraints into CNF such that generalized arc consistency is maintained. In Proceedings of KI 2014, volume 8736 of LNCS, pages 123-134. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-11206-0_13.
http://dx.doi.org/10.1007/978-3-319-11206-0_13
Olivier Roussel and Vasco M. Manquinho. Pseudo-Boolean and cardinality constraints. In Handbook of Satisfiability, pages 695-733. IOS, 2009. URL: http://dx.doi.org/10.3233/978-1-58603-929-5-695.
http://dx.doi.org/10.3233/978-1-58603-929-5-695
Patrik Simons, Ilkka Niemelä, and Timo Soininen. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2):181-234, 2002. URL: http://dx.doi.org/10.1016/S0004-3702(02)00187-X.
http://dx.doi.org/10.1016/S0004-3702(02)00187-X
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Justifications and Blocking Sets in a Rule-Based Answer Set Computation
Notions of justifications for logic programs under answer set semantics have been recently studied for atom-based approaches or argumentation approaches. The paper addresses the question in a rule-based answer set computation: the search algorithm does not guess on the truth or falsity of an atom but on the application or non application of a non monotonic rule. In this view, justifications are sets of ground rules with particular properties. Properties of these justifications are established; in particular the notion of blocking set (a reason incompatible with an answer set) is defined, that permits to explain computation failures. Backjumping, learning, debugging and explanations are possible applications.
Answer Set Programming
Justification
Rule-based Computation
6:1-6:15
Regular Paper
Christopher
Béatrix
Christopher Béatrix
Claire
Lefèvre
Claire Lefèvre
Laurent
Garcia
Laurent Garcia
Igor
Stéphan
Igor Stéphan
10.4230/OASIcs.ICLP.2016.6
C. V. Damásio, A. Analyti, and G. Antoniou. Justifications for logic programming. In LPNMR 2013,, pages 530-542, 2013.
C. V. Damásio, J. Moura, and A. Analyti. Unifying justifications and debugging for answer-set programs. In ICLP 2015, 2015.
M. Dao-Tran, T. Eiter, M. Fink, G. Weidinger, and A. Weinzierl. OMiGA: An open minded grounding on-the-fly answer set solver. In JELIA 2012, pages 480-483, 2012.
T. Eiter, M. Fink, P. Schüller, and A. Weinzierl. Finding explanations of inconsistency in multi-context systems. In KR 2010, 2010.
M. Gebser, B. Kaufmann, A. Neumann, and T. Schaub. Conflict-driven answer set solving. In IJCAI 2007, pages 386-392, 2007.
M. Gebser, J. Pührer, T. Schaub, and H. Tompits. A meta-programming technique for debugging answer-set programs. In AAAI 2008, pages 448-453, 2008.
M. Gelfond and V. Lifschitz. The stable model semantics for logic programming. In Logic Programming, Proceedings of the Fifth International Conference and Symposium, pages 1070-1080, 1988.
K. Konczak, T. Linke, and T. Schaub. Graphs and colorings for answer set programming. Theory and Practice of Logic Programming, 6:61-106, 1 2006. URL: http://dx.doi.org/10.1017/S1471068405002528.
http://dx.doi.org/10.1017/S1471068405002528
C. Lefèvre, C. Béatrix, I. Stéphan, and L. Garcia. Asperix, a first order forward chaining approach for answer set computing. CoRR, abs/1503.07717:(to appear in TPLP), 2015. URL: http://arxiv.org/abs/1503.07717.
http://arxiv.org/abs/1503.07717
C. Lefèvre and P. Nicolas. A first order forward chaining approach for answer set computing. In LPNMR 2009, pages 196-208, 2009.
C. Lefèvre and P. Nicolas. The first version of a new ASP solver : ASPeRiX. In LPNMR 2009, pages 522-527, 2009.
N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri, and F. Scarcello. The DLV system for knowledge representation and reasoning. ACM Transactions on Computational Logic, 7(3):499-562, 2006. URL: http://dx.doi.org/10.1145/1149114.1149117.
http://dx.doi.org/10.1145/1149114.1149117
L. Liu, E. Pontelli, T. C. Son, and M. Truszczynski. Logic programs with abstract constraint atoms: The role of computations. Artificial Intelligence, 174(3-4):295-315, 2010. URL: http://dx.doi.org/10.1016/j.artint.2009.11.016.
http://dx.doi.org/10.1016/j.artint.2009.11.016
J. Oetsch, J. Pührer, and H. Tompits. Stepping through an answer-set program. In LPNMR 2011, pages 134-147, 2011.
A. Dal Palù, A. Dovier, E. Pontelli, and G. Rossi. Answer set programming with constraints using lazy grounding. In ICLP 2009, 2009.
E. Pontelli, T. C. Son, and O. El-Khatib. Justifications for logic programs under answer set semantics. Theory and Practice of Logic Programming, 9(1):1-56, 2009. URL: http://dx.doi.org/10.1017/S1471068408003633.
http://dx.doi.org/10.1017/S1471068408003633
C. Schulz and F. Toni. Justifying answer sets using argumentation. Theory and Practice of Logic Programming, 16(1):59-110, 2016. URL: http://dx.doi.org/10.1017/S1471068414000702.
http://dx.doi.org/10.1017/S1471068414000702
P. Simons, I. Niemelä, and T. Soininen. Extending and implementing the stable model semantics. Artificial Intelligence, 138(1-2):181-234, 2002. URL: http://dx.doi.org/10.1016/S0004-3702(02)00187-X.
http://dx.doi.org/10.1016/S0004-3702(02)00187-X
A. Weinzierl. Learning non-ground rules for answer-set solving. In 2nd Workshop on Grounding and Transformations for Theories with Variables, GTTV 2013, 2013.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Intelligent Instantiation and Supersafe Rules
In the input languages of most answer set solvers, a rule with variables has, conceptually, infinitely many instances. The primary role of the process of intelligent instillation is to identify a finite set of ground instances of rules of the given program that are "essential" for generating its stable models. This process can be launched only when all rules of the program are safe. If a program contains arithmetic operations or comparisons then its rules are expected to satisfy conditions that are even stronger than safety. This paper is an attempt to make the idea of an essential instance and the need for "supersafety" in the process of intelligent instantiation mathematically
precise.
answer set programming
7:1-7:14
Regular Paper
Vladimir
Lifschitz
Vladimir Lifschitz
10.4230/OASIcs.ICLP.2016.7
Evgenii Balai, Michael Gelfond, and Yuanlin Zhang. Towards answer set programming with sorts. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pages 135-147, 2013.
Annamaria Bria, Wolfgang Faber, and Nicola Leone. Normal form nested programs. In Proceedings of European Conference on Logics in Artificial Intelligence (JELIA), 2008.
Pedro Cabalar, David Pearce, and Agustin Valverde. A revised concept of safety for general answer set programs. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), 2009.
Francesco Calimeri, Susanna Cozza, Giovambattista Ianni, and Nicola Leone. Computable functions in ASP: theory and implementation. In Proceedings of International Conference on Logic Programming (ICLP), pages 407-424, 2008.
Martin Gebser, Amelia Harrison, Roland Kaminski, Vladimir Lifschitz, and Torsten Schaub. Abstract Gringo. Theory and Practice of Logic Programming, 15:449-463, 2015.
Joohyung Lee, Vladimir Lifschitz, and Ravi Palla. Safe formulas in the general theory of stable models (preliminary report). In Proceedings of International Conference on Logic Programming (ICLP), pages 672-676, 2008.
Vladimir Lifschitz, Lappoon R. Tang, and Hudson Turner. Nested expressions in logic programs. Annals of Mathematics and Artificial Intelligence, 25:369-389, 1999.
Yuri Matiyasevich. Hilbert’s Tenth Problem. MIT Press, 1993.
Norman McCain and Hudson Turner. Language independence and language tolerance in logic programs. In Pascal Van Hentenryck, editor, Proceedings Eleventh International Conference on Logic Programming, pages 38-57, 1994.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
An Answer Set Programming Framework for Reasoning About Truthfulness of Statements by Agents
We propose a framework for answering the question of whether statements made by an agent can be believed, in light of observations made over time. The basic components of the framework are a formalism for reasoning about actions, changes, and observations and a formalism for default reasoning. The framework is suitable for concrete implementation, e.g., using answer set programming for asserting the truthfulness of statements made by agents, starting from observations, knowledge about the actions of the agents, and a theory about the "normal" behavior of agents.
Agents
ASP
Reasoning
Knowledge
8:1-8:4
Regular Paper
Tran
Cao Son
Tran Cao Son
Enrico
Pontelli
Enrico Pontelli
Michael
Gelfond
Michael Gelfond
Marcello
Balduccini
Marcello Balduccini
10.4230/OASIcs.ICLP.2016.8
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Answer Set Solving with Generalized Learned Constraints
Conflict learning plays a key role in modern Boolean constraint solving. Advanced in satisfiability testing, it has meanwhile become a base technology in many neighboring fields, among them answer set programming (ASP). However, learned constraints are only valid for a currently solved problem instance and do not carry over to similar instances. We address this issue in ASP and introduce a framework featuring an integrated feedback loop that allows for reusing conflict constraints. The idea is to extract (propositional) conflict constraints, generalize and validate them, and reuse them as integrity constraints. Although we explore our approach in the context of dynamic applications based on transition systems, it is driven by the ultimate objective of overcoming the issue that learned knowledge is bound to specific problem instances. We implemented this workflow in two systems, namely, a variant of the ASP solver clasp that extracts integrity constraints along with a downstream system for generalizing and validating them.
Answer Set Programming
Conflict Learning
Constraint Generalization
Generalized Constraint Feedback
9:1-9:15
Regular Paper
Martin
Gebser
Martin Gebser
Roland
Kaminski
Roland Kaminski
Benjamin
Kaufmann
Benjamin Kaufmann
Patrick
Lühne
Patrick Lühne
Javier
Romero
Javier Romero
Torsten
Schaub
Torsten Schaub
10.4230/OASIcs.ICLP.2016.9
M. Alviano, C. Dodaro, N. Leone, and F. Ricca. Advances in WASP. In F. Calimeri, G. Ianni, and M. Truszczyński, editors, Proceedings of the Thirteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'15), pages 40-54. Springer, 2015.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
G. Brewka, T. Eiter, and M. Truszczyński. Answer set programming at a glance. Communications of the ACM, 54(12):92-103, 2011.
F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, F. Ricca, and T. Schaub. ASP-Core-2: Input language format. Available at https://www.mat.unical.it/aspcomp2013/ASPStandardization/, 2012.
https://www.mat.unical.it/aspcomp2013/ASPStandardization/
J. Charnley, S. Colton, and I. Miguel. Automated generation of implied constraints. In G. Brewka, S. Coradeschi, A. Perini, and P. Traverso, editors, Proceedings of the Seventeenth European Conference on Artificial Intelligence (ECAI'06), pages 73-77. IOS Press, 2006.
M. Dao-Tran, T. Eiter, M. Fink, G. Weidinger, and A. Weinzierl. OMiGA : An open minded grounding on-the-fly answer set solver. In L. Fariñas del Cerro, A. Herzig, and J. Mengin, editors, Proceedings of the Thirteenth European Conference on Logics in Artificial Intelligence (JELIA'12), pages 480-483. Springer, 2012.
B. De Cat and M. Bruynooghe. Detection and exploitation of functional dependencies for model generation. Theory and Practice of Logic Programming, 13(4-5):471-485, 2013.
R. Dechter. Constraint Processing. Morgan Kaufmann Publishers, 2003.
M. Gebser, R. Kaminski, B. Kaufmann, P. Lühne, J. Romero, and T. Schaub. Answer set solving with generalized learned constraints (extended version). Available at http://www.cs.uni-potsdam.de/wv/publications/, 2016.
http://www.cs.uni-potsdam.de/wv/publications/
M. Gebser, R. Kaminski, M. Knecht, and T. Schaub. plasp: A prototype for PDDL-based planning in ASP. In J. Delgrande and W. Faber, editors, Proceedings of the Eleventh International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'11), pages 358-363. Springer, 2011.
M. Gebser, B. Kaufmann, and T. Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012.
M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases. New Generation Computing, 9:365-385, 1991.
E. Giunchiglia, Y. Lierler, and M. Maratea. Answer set programming based on propositional satisfiability. Journal of Automated Reasoning, 36(4):345-377, 2006.
S. Haufe, S. Schiffel, and M. Thielscher. Automated verification of state sequence invariants in general game playing. Artificial Intelligence, 187-188:1-30, 2012.
M. Helmert. Concise finite-domain representations for PDDL planning tasks. Artificial Intelligence, 173(5-6):503-535, 2009.
M. Law, A. Russo, and K. Broda. Inductive learning of answer set programs. In E. Fermé and J. Leite, editors, Proceedings of the Fourteenth European Conference on Logics in Artificial Intelligence (JELIA'14), pages 311-325. Springer, 2014.
V. Lifschitz. Answer set programming and plan generation. Artificial Intelligence, 138(1-2):39-54, 2002.
F. Lin. Discovering state invariants. In D. Dubois, C. Welty, and M. Williams, editors, Proceedings of the Ninth International Conference on Principles of Knowledge Representation and Reasoning (KR'04), pages 536-544. AAAI Press, 2004.
P. Lühne. Generalizing learned knowledge in answer set solving. Master’s thesis, Hasso Plattner Institute, Potsdam, 2015.
J. Marques-Silva and K. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, 1999.
B. O'Sullivan. Automated modelling and solving in constraint programming. In M. Fox and D. Poole, editors, Proceedings of the Twenty-fourth National Conference on Artificial Intelligence (AAAI'10), pages 1493-1497. AAAI Press, 2010.
R. Otero. Induction of stable models. In C. Rouveirol and M. Sebag, editors, Proceedings of the Eleventh International Conference on Inductive Logic Programming (ILP'01), pages 193-205. Springer, 2001.
J. Rintanen. An iterative algorithm for synthesizing invariants. In Proceedings of the Seventeenth National Conference on Artificial Intelligence (AAAI'00), pages 806-811. AAAI/MIT Press, 2000.
M. Sheeran, S. Singh, and G. Stålmarck. Checking safety properties using induction and a SAT-solver. In W. Hunt and S. Johnson, editors, Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD'00), pages 108-125. Springer, 2000.
Y. Vizel, G. Weissenbacher, and S. Malik. Boolean satisfiability solvers and their applications in model checking. Proceedings of the IEEE, 103(11):2021-2035, 2015.
A. Weinzierl. Learning non-ground rules for answer-set solving. In D. Pearce, S. Tasharrofi, E. Ternovska, and C. Vidal, editors, Proceedings of the Second Workshop on Grounding and Transformation for Theories with Variables (GTTV'13), pages 25-37, 2013.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
P-rho-Log: Combining Logic Programming with Conditional Transformation Systems
P-rho-Log extends Prolog by conditional transformations that are controlled by strategies. We give a brief overview of the tool and illustrate its capabilities.
Conditional transformation rules
strategies
Prolog
10:1-10:5
Regular Paper
Besik
Dundua
Besik Dundua
Temur
Kutsia
Temur Kutsia
Klaus
Reisenberger-Hagmayer
Klaus Reisenberger-Hagmayer
10.4230/OASIcs.ICLP.2016.10
Emilie Balland, Paul Brauner, Radu Kopetz, Pierre-Etienne Moreau, and Antoine Reilles. Tom: Piggybacking rewriting on Java. In Franz Baader, editor, Term Rewriting and Applications, 18th International Conference, RTA 2007, volume 4533 of Lecture Notes in Computer Science, pages 36-47. Springer, 2007.
Peter Borovanský, Claude Kirchner, Hélène Kirchner, Pierre-Etienne Moreau, and Marian Vittek. Elan: A logical framework based on computational systems. ENTCS, 4, 1996.
Stefan D. Bruda. Prolog mode for Emacs (version 1.25), 2003. Available from https://bruda.ca/emacs/prolog_mode_for_emacs.
Yves Caseau, François-Xavier Josset, and François Laburthe. CLAIRE: combining sets, search and rules to better express algorithms. TPLP, 2(6):769-805, 2002.
Horatiu Cirstea and Claude Kirchner. The rewriting calculus - Parts I and II. Logic Journal of the IGPL, 9(3):339-410, 2001.
Manuel Clavel, Francisco Durán, Steven Eker, Patrick Lincoln, Narciso Martí-Oliet, José Meseguer, and Jose F. Quesada. Maude: specification and programming in rewriting logic. Theor. Comput. Sci., 285(2):187-243, 2002.
Jorge Coelho, Besik Dundua, Mário Florido, and Temur Kutsia. A rule-based approach to XML processing and web reasoning. In Pascal Hitzler and Thomas Lukasiewicz, editors, RR 2010, volume 6333 of LNCS, pages 164-172. Springer, 2010.
Hubert Comon. Completion of rewrite systems with membership constraints. Part II: Constraint solving. J. Symb. Comput., 25(4):421-453, 1998.
Besik Dundua, Temur Kutsia, and Mircea Marin. Strategies in PρLog. In Maribel Fernández, editor, 9th Int. Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009, volume 15 of EPTCS, pages 32-43, 2009.
Besik Dundua, Temur Kutsia, and Klaus Reisenberger-Hagmayer. An overview of PρLog. RISC Report Series 16-05, Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria, 2016.
Thom W. Frühwirth. Theory and practice of Constraint Handling Rules. J. Log. Program., 37(1-3):95-138, 1998.
Temur Kutsia. Solving and Proving in Equational Theories with Sequence Variables and Flexible Arity Symbols. RISC Report Series 02-09, RISC, University of Linz, 2002. PhD Thesis.
Temur Kutsia and Mircea Marin. Matching with regular constraints. In Geoff Sutcliffe and Andrei Voronkov, editors, LPAR, volume 3835 of Lecture Notes in Computer Science, pages 215-229. Springer, 2005.
John Lloyd. Foundations of Logic Programming. Springer-Verlag, 2nd edition, 1987.
Mircea Marin and Temur Kutsia. Foundations of the rule-based system ρLog. Journal of Applied Non-Classical Logics, 16(1-2):151-168, 2006.
Mark van den Brand, Arie van Deursen, Jan Heering, Hayco de Jong, Merijn de Jonge, Tobias Kuipers, Paul Klint, Leon Moonen, Pieter A. Olivier, Jeroen Scheerder, Jurgen J. Vinju, Eelco Visser, and Joost Visser. The Asf+Sdf meta-environment: a component-based language development environment. Electr. Notes Theor. Comput. Sci., 44(2):3-8, 2001.
Eelco Visser. Stratego: A language for program transformation based on rewriting strategies. In Aart Middeldorp, editor, Rewriting Techniques and Applications, 12th International Conference, RTA 2001, volume 2051 of Lecture Notes in Computer Science, pages 357-362. Springer, 2001.
Jan Wielemaker, Tom Schrijvers, Markus Triska, and Torbjörn Lager. SWI-Prolog. Theory and Practice of Logic Programming, 12(1-2):67-96, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Grounded Fixpoints and Active Integrity Constraints
The formalism of active integrity constraints was introduced as a way to specify particular classes of integrity constraints over relational databases together with preferences on how to repair existing inconsistencies. The rule-based syntax of such integrity constraints also provides algorithms for finding such repairs that achieve the best asymptotic complexity.
However, the different semantics that have been proposed for these integrity constraints all exhibit some counter-intuitive examples. In this work, we look at active integrity constraints using ideas from algebraic fixpoint theory. We show how database repairs can be modeled as fixpoints of particular operators on databases, and study how the notion of grounded fixpoint induces a corresponding notion of grounded database repair that captures several natural intuitions, and in particular avoids the problems of previous alternative semantics.
In order to study grounded repairs in their full generality, we need to generalize the notion of grounded fixpoint to non-deterministic operators. We propose such a definition and illustrate its plausibility in the database context.
grounded fixpoints
active integrity constraints
11:1-11:14
Regular Paper
Luís
Cruz-Filipe
Luís Cruz-Filipe
10.4230/OASIcs.ICLP.2016.11
Serge Abiteboul. Updates, a new frontier. In Marc Gyssens, Jan Paredaens, and Dirk van Gucht, editors, ICDT, volume 326 of LNCS, pages 1-18. Springer, 1988.
Serge Abiteboul, Richard Hull, and Victor Vianu. Foundations of Databases. Addison Wesley, 1995.
Grigoris Antoniou. A tutorial on default logics. ACM Computing Surveys, 31(3):337-359, 1999.
Catriel Beeri and Moshe Y. Vardi. The implication problem for data dependencies. In Colloquium on Automata, Languages and Programming, pages 73-85, London, UK, 1981. Springer.
Bart Bogaerts, Joost Vennekens, and Marc Denecker. Grounded fixpoints and their applications in knowledge representation. Artif. Intell., 224:51-71, 2015.
Luciano Caroprese, Sergio Greco, Cristina Sirangelo, and Ester Zumpano. Declarative semantics of production rules for integrity maintenance. In Sandro Etalle and Miroslaw Truszczynski, editors, ICLP, volume 4079 of LNCS, pages 26-40. Springer, 2006.
Luciano Caroprese and Miroslaw Truszczynski. Active integrity constraints and revision programming. Theory Pract. Log. Program., 11(6):905-952, November 2011.
Luís Cruz-Filipe. Optimizing computation of repairs from active integrity constraints. In Christoph Beierle and Carlo Meghini, editors, FoIKS, volume 8367 of LNCS, pages 361-380. Springer, 2014.
Luís Cruz-Filipe, Patrícia Engrácia, Graça Gaspar, and Isabel Nunes. Computing repairs from active integrity constraints. In Hai Wang and Richard Banach, editors, TASE, pages 183-190. IEEE, July 2013.
Luís Cruz-Filipe, Michael Franz, Artavazd Hakhverdyan, Marta Ludovico, Isabel Nunes, and Peter Schneider-Kamp. repAIrC: A tool for ensuring data consistency by means of active integrity constraints. In Ana L.N. Fred, Jan L.G. Dietz, David Aveiro, Kecheng Liu, and Joaquim Filipe, editors, KMIS, pages 17-26. SciTePress, 2015.
Luís Cruz-Filipe, Isabel Nunes, and Peter Schneider-Kamp. Integrity constraints for general-purpose knowledge bases. In Marc Gyssens and Guillermo Ricardo Simari, editors, FoIKS, volume 9616 of LNCS, pages 235-254. Springer, 2016.
Thomas Eiter and Georg Gottlob. On the complexity of propositional knowledge base revision, updates, and counterfactuals. Artif. Intell., 57(2-3):227-270, 1992.
Melvin Fitting. Fixpoint semantics for logic programming: a survey. Theor. Comput. Sci., 278(1-2):25-51, 2002.
Sergio Flesca, Sergio Greco, and Ester Zumpano. Active integrity constraints. In Eugenio Moggi and David Scott Warren, editors, PPDP, pages 98-107. ACM, 2004.
Ahmed Guessoum. Abductive knowledge base updates for contextual reasoning. J. Intell. Inf. Syst., 11(1):41-67, 1998.
Mohammed A. Khamsi, Vladik Kreinovich, and Driss Misane. A new method of proving the existence of answer sets for disjunctive logic programs. In Proceedings of the Workshop on Logic Programming with Incomplete Information, 1993.
V. Wiktor Marek and Miroslav Truszczynski. Revision programming, database updates and integrity constraints. In Georg Gottlob and Moshe Y. Vardi, editors, ICDT, volume 893 of LNCS, pages 368-382. Springer, 1995.
Enric Mayol and Ernest Teniente. Addressing efficiency issues during the process of integrity maintenance. In Trevor J.M. Bench-Capon, Giovanni Soda, and A Min Tjoa, editors, DEXA, volume 1677 of LNCS, pages 270-281. Springer, 1999.
Shamim A. Naqvi and Ravi Krishnamurthy. Database updates in logic programming. In Chris Edmondson-Yurkanan and Mihalis Yannakakis, editors, PODS, pages 251-262. ACM, 1988.
Teodor C. Przymusinski and Hudson Turner. Update by means of inference rules. J. Log. Program., 30(2):125-143, 1997.
Raymond Reiter. A logic for default reasoning. Artificial Intelligence, 13:81-132, 1980.
Ernest Teniente and Antoni Olivé. Updating knowledge bases while maintaining their consistency. VLDB J., 4(2):193-241, 1995.
Jennifer Widom and Stefano Ceri, editors. Active Database Systems: Triggers and Rules For Advanced Database Processing. Morgan Kaufmann, 1996.
Marianne Winslett. Updating Logical Databases. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Constraint CNF: SAT and CSP Language Under One Roof
A new language, called constraint CNF, is proposed. It integrates propositional logic with constraints stemming from constraint programming. A family of algorithms is designed to solve problems expressed in constraint CNF. These algorithms build on techniques from both propositional satisfiability and constraint programming. The result is a uniform language and an algorithmic framework, which allow us to gain a deeper understanding of the relation between the solving techniques used in propositional satisfiability and in constraint programming and apply them together.
Propositional Satisfiability
Constraint Programming
12:1-12:15
Regular Paper
Broes
De Cat
Broes De Cat
Yuliya
Lierler
Yuliya Lierler
10.4230/OASIcs.ICLP.2016.12
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Constraint Propagation and Explanation over Novel Types by Abstract Compilation
The appeal of constraint programming (CP) lies in compositionality – the ability to mix and match constraints as needed. However, this flexibility typically does not extend to the types of variables. Solvers usually support only a small set of pre-defined variable types, and extending this is not typically a simple exercise: not only must the solver engine be updated, but then the library of supported constraints must be re-implemented to support the new type.
In this paper, we attempt to ease this second step. We describe a system for automatically deriving a native-code implementation of a global constraint (over novel variable types) from a declarative specification, complete with the ability to explain its propagation, a requirement if we want to make use of modern lazy clause generation CP solvers.
We demonstrate this approach by adding support for wrapped-integer variables to chuffed, a lazy clause generation CP solver.
constraint programming
program synthesis
program analysis
13:1-13:14
Regular Paper
Graeme
Gange
Graeme Gange
Peter J.
Stuckey
Peter J. Stuckey
10.4230/OASIcs.ICLP.2016.13
Sébastien Bardin, Philippe Herrmann, and Florian Perroud. An Alternative to SAT-Based Approaches for Bit-Vectors. In Tools and Algorithms for the Construction and Analysis of Systems, number 6015 in LNCS, pages 84-98. Springer Berlin Heidelberg, March 2010.
Ralph Becket. Specification of FlatZinc. [Online, accessed 3 March 2015], 2012. URL: http://www.minizinc.org/downloads/doc-1.6/flatzinc-spec.pdf.
http://www.minizinc.org/downloads/doc-1.6/flatzinc-spec.pdf
N. Beldiceanu, M. Carlsson, and T. Petit. Deriving filtering algorithms from constraint checkers. In CP 2014, volume 3258, pages 107-122, 2004. URL: http://dx.doi.org/10.1007/978-3-540-30201-8_11.
http://dx.doi.org/10.1007/978-3-540-30201-8_11
Sebastian Brand and Roland H. C. Yap. Towards `propagation = logic + control'. In ICLP 2006, volume 4079, pages 102-116, 2006. URL: http://dx.doi.org/10.1007/11799573_10.
http://dx.doi.org/10.1007/11799573_10
Rafael Caballero, Peter J. Stuckey, and Antonio Tenorio-Fornes. Two type extensions for the constraint modelling language MiniZinc. Science of Computer Programming, 111:156-189, 2016.
Geoffrey Chu. Improving Combinatorial Optimization. PhD thesis, Department of Computing and Information Systems, University of Melbourne, 2011.
Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL'77, pages 238-252, New York, NY, USA, 1977. URL: http://dx.doi.org/10.1145/512950.512973.
http://dx.doi.org/10.1145/512950.512973
Patrick Cousot and Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In PLILP'92, volume 631, pages 269-295, 1992.
Patrick Cousot, Radhia Cousot, and Francesco Logozzo. Precondition Inference from Intermittent Assertions and Application to Contracts on Collections. In VMCAI 2011, number 6538 in LNCS, pages 150-168. Springer Berlin Heidelberg, January 2011.
William Craig. Three uses of the herbrand-gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic, 22:269-285, 9 1957. URL: http://dx.doi.org/10.2307/2963594.
http://dx.doi.org/10.2307/2963594
Tristan Denmat, Arnaud Gotlieb, and Mireille Ducassé. An abstract interpretation based combinator for modelling while loops in constraint programming. In CP 2013, volume 4741, pages 241-255, 2007. URL: http://dx.doi.org/10.1007/978-3-540-74970-7_19.
http://dx.doi.org/10.1007/978-3-540-74970-7_19
Ian P. Gent, Christopher Jefferson, Steve Linton, Ian Miguel, and Peter Nightingale. Generating custom propagators for arbitrary constraints. Artif. Intell., 211:1-33, 2014. URL: http://dx.doi.org/10.1016/j.artint.2014.03.001.
http://dx.doi.org/10.1016/j.artint.2014.03.001
Arnaud Gotlieb, Michel Leconte, and Bruno Marre. Constraint solving on modular integers. In ModRef Workshop, associated to CP'2010, September 2010.
C. Lattner and V. Adve. LLVM: a compilation framework for lifelong program analysis transformation. In CGO 2004, pages 75-86, March 2004. URL: http://dx.doi.org/10.1109/CGO.2004.1281665.
http://dx.doi.org/10.1109/CGO.2004.1281665
Christopher Mears, Andreas Schutt, Peter J. Stuckey, Guido Tack, Kim Marriott, and Mark Wallace. Modelling with option types in minizinc. In CPAIOR 2014, number 8451 in LNCS, pages 88-103. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-07046-9_7.
http://dx.doi.org/10.1007/978-3-319-07046-9_7
Jean-Noël Monette, Pierre Flener, and Justin Pearson. Towards solver-independent propagators. In CP 2012, volume 7514, pages 544-560, 2012. URL: http://dx.doi.org/10.1007/978-3-642-33558-7_40.
http://dx.doi.org/10.1007/978-3-642-33558-7_40
O. Ohrimenko, P.J. Stuckey, and M. Codish. Propagation via lazy clause generation. Constraints, 14(3):357-391, 2009.
Marie Pelleau, Antoine Miné, Charlotte Truchet, and Frédéric Benhamou. A Constraint Solver Based on Abstract Domains. In VMCAI 2013, number 7737 in LNCS, pages 434-454. Springer Berlin Heidelberg, January 2013.
P. Van Hentenryck, Vijay Saraswat, and Yves Deville. Constraint processing in cc(FD). Technical report, Computer Science Department, Brown University, 1992.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
A Compositional Typed Higher-Order Logic with Definitions
Expressive KR languages are built by integrating different language constructs, or extending a language with new language constructs. This process is difficult if non-truth-functional or non-monotonic constructs are involved. What is needed is a compositional principle.
This paper presents a compositional principle for defining logics by modular composition of logical constructs, and applies it to build a higher order logic integrating typed lambda calculus and rule sets under a well-founded or stable semantics. Logical constructs are formalized as triples of a syntactical rule, a semantical rule, and a typing rule. The paper describes how syntax, typing and semantics of the logic are composed from the set of its language constructs. The base semantical concept is the infon: mappings from structures to values in these structures. Semantical operators of language constructs operate on infons and allow to construct the infons of compound expressions from the infons of its subexpressions. This conforms to Frege's principle of compositionality.
Logic
Semantics
Compositionality
14:1-14:13
Regular Paper
Ingmar
Dasseville
Ingmar Dasseville
Matthias
van der Hallen
Matthias van der Hallen
Bart
Bogaerts
Bart Bogaerts
Gerda
Janssens
Gerda Janssens
Marc
Denecker
Marc Denecker
10.4230/OASIcs.ICLP.2016.14
H. Abramson and H. Rogers. Meta-programming in logic programming. MIT Press, 1989.
Jon Barwise and John Etchemendy. Information, infons, and inference. Situation theory and its applications, 1(22), 1990.
Bart Bogaerts. Groundedness in logics with a fixpoint semantics. PhD thesis, Informatics Section, Department of Computer Science, Faculty of Engineering Science, June 2015. Denecker, Marc (supervisor), Vennekens, Joost and Van den Bussche, Jan (cosupervisors). URL: https://lirias.kuleuven.be/handle/123456789/496543.
https://lirias.kuleuven.be/handle/123456789/496543
Weidong Chen, Michael Kifer, and David S Warren. Hilog: A foundation for higher-order logic programming. The Journal of Logic Programming, 15(3):187-230, 1993.
Ingmar Dasseville, Matthias van der Hallen, Gerda Janssens, and Marc Denecker. Semantics of templates in a compositional framework for building logics. TPLP, 15(4-5):681-695, 2015. URL: http://dx.doi.org/10.1017/S1471068415000319.
http://dx.doi.org/10.1017/S1471068415000319
Marc Denecker, Victor Marek, and Mirosław Truszczyński. Approximations, stable operators, well-founded fixpoints and applications in nonmonotonic reasoning. In Jack Minker, editor, Logic-Based Artificial Intelligence, volume 597 of The Springer International Series in Engineering and Computer Science, pages 127-144. Springer US, 2000. URL: http://dx.doi.org/10.1007/978-1-4615-1567-8_6.
http://dx.doi.org/10.1007/978-1-4615-1567-8_6
Marc Denecker and Eugenia Ternovska. A logic of nonmonotone inductive definitions. ACM Trans. Comput. Log., 9(2):14:1-14:52, April 2008. URL: http://dx.doi.org/10.1145/1342991.1342998.
http://dx.doi.org/10.1145/1342991.1342998
Keith Devlin. Logic and information. Cambridge University Press, 1991.
Wolfgang Faber, Gerald Pfeifer, and Nicola Leone. Semantics and complexity of recursive aggregates in answer set programming. Artif. Intell., 175(1):278-298, 2011. URL: http://dx.doi.org/10.1016/j.artint.2010.04.002.
http://dx.doi.org/10.1016/j.artint.2010.04.002
Paolo Ferraris. Answer sets for propositional theories. In Proceedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pages 119-131, 2005. URL: http://dx.doi.org/10.1007/11546207_10.
http://dx.doi.org/10.1007/11546207_10
Michael Gelfond and Yuanlin Zhang. Vicious circle principle and logic programs with aggregates. TPLP, 14(4-5):587-601, 2014. URL: http://dx.doi.org/10.1017/S1471068414000222.
http://dx.doi.org/10.1017/S1471068414000222
Tias Guns. Declarative pattern mining using constraint programming. Constraints, 20(4):492-493, 2015.
Yuri Gurevich and Itay Neeman. Logic of infons: The propositional case. ACM Trans. Comput. Log., 12(2):9, 2011. URL: http://dx.doi.org/10.1145/1877714.1877715.
http://dx.doi.org/10.1145/1877714.1877715
Jerry R Hobbs and Stanley J Rosenschein. Making computational sense of montague’s intensional logic. Artificial Intelligence, 9(3):287-306, 1977.
David B. Kemp and Peter J. Stuckey. Semantics of logic programs with aggregates. In Vijay A. Saraswat and Kazunori Ueda, editors, ISLP, pages 387-401. MIT Press, 1991.
Javier Leach, Susana Nieva, and Mario Rodríguez-Artalejo. Constraint logic programming with hereditary harrop formula. CoRR, cs.PL/0404053, 2004.
Vladimir Lifschitz. Answer set planning. In Danny De Schreye, editor, Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29 - December 4, 1999, pages 23-37. MIT Press, 1999.
Victor Marek and Mirosław Truszczyński. Stable models and an alternative logic programming paradigm. In Krzysztof R. Apt, Victor Marek, Mirosław Truszczyński, and David S. Warren, editors, The Logic Programming Paradigm: A 25-Year Perspective, pages 375-398. Springer-Verlag, 1999. URL: http://arxiv.org/abs/cs.LO/9809032.
http://arxiv.org/abs/cs.LO/9809032
Gopalan Nadathur and Dale Miller. An overview of LambdaProlog. In Fifth International Conference and Symposium on Logic Programming. MIT Press, 1988.
Ilkka Niemelä. Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell., 25(3-4):241-273, 1999. URL: http://dx.doi.org/10.1023/A:1018930122475.
http://dx.doi.org/10.1023/A:1018930122475
Nikolay Pelov, Marc Denecker, and Maurice Bruynooghe. Well-founded and stable semantics of logic programs with aggregates. TPLP, 7(3):301-353, 2007. URL: http://dx.doi.org/10.1017/S1471068406002973.
http://dx.doi.org/10.1017/S1471068406002973
Tran Cao Son, Enrico Pontelli, and Islam Elkabani. An unfolding-based semantics for logic programming with aggregates. CoRR, abs/cs/0605038, 2006. URL: http://arxiv.org/abs/cs/0605038.
http://arxiv.org/abs/cs/0605038
Shahab Tasharrofi and Eugenia Ternovska. A semantic account for modularity in multi-language modelling of search problems. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings, volume 6989 of Lecture Notes in Computer Science, pages 259-274. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-24364-6_18.
http://dx.doi.org/10.1007/978-3-642-24364-6_18
Shahab Tasharrofi and Eugenia Ternovska. Three semantics for modular systems. CoRR, abs/1405.1229, 2014. URL: http://arxiv.org/abs/1405.1229.
http://arxiv.org/abs/1405.1229
Allen Van Gelder. The well-founded semantics of aggregation. In PODS, pages 127-138. ACM Press, 1992. URL: http://dx.doi.org/10.1145/137097.137854.
http://dx.doi.org/10.1145/137097.137854
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Inference in Probabilistic Logic Programs Using Lifted Explanations
In this paper, we consider the problem of lifted inference in the context of Prism-like probabilistic logic programming languages. Traditional inference in such languages involves the construction of an explanation graph for the query that treats each instance of a random variable separately. For many programs and queries, we observe that explanations can be summarized into substantially more compact structures introduced in this paper, called "lifted explanation graph". In contrast to existing lifted inference techniques, our method for constructing lifted explanations naturally generalizes existing methods for constructing explanation graphs. To compute probability of query answers, we solve recurrences generated from the lifted graphs. We show examples where the use of our technique reduces the asymptotic complexity of inference.
Probabilistic logic programs
Probabilistic inference
Lifted inference
Symbolic evaluation
Constraints
15:1-15:15
Regular Paper
Arun
Nampally
Arun Nampally
C. R.
Ramakrishnan
C. R. Ramakrishnan
10.4230/OASIcs.ICLP.2016.15
Elena Bellodi, Evelina Lamma, Fabrizio Riguzzi, Vítor Santos Costa, and Riccardo Zese. Lifted variable elimination for probabilistic logic programming. TPLP, 14(4-5):681-695, 2014.
Rodrigo De Salvo Braz, Eyal Amir, and Dan Roth. Lifted first-order probabilistic inference. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence, pages 1319-1325, 2005.
Randal E Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR), 24(3):293-318, 1992.
Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. ProbLog: A probabilistic prolog and its application in link discovery. In IJCAI, pages 2462-2467, 2007.
Anton Dries, Angelika Kimmig, Wannes Meert, Joris Renkens, Guy Van den Broeck, Jonas Vlasselaer, and Luc De Raedt. Problog2: Probabilistic logic programming. In ECML PKDD, pages 312-315, 2015.
Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Efficient verification of real-time systems: Compact data structure and state-space reduction. In IEEE RTSS’97, pages 14-24, 1997.
Brian Milch, Luke S Zettlemoyer, Kristian Kersting, Michael Haimes, and Leslie Pack Kaelbling. Lifted probabilistic inference with counting formulas. In Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, pages 1062-1068, 2008.
Antoine Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19(1):31-100, 2006.
Arun Nampally and C. R. Ramakrishnan. Inference in probabilistic logic programs using lifted explanations. Technical report, Computer Science Department, Stony Brook University, 2016. URL: http://www.cs.stonybrook.edu/~px/Papers/NR:lifted_tr_2016/.
http://www.cs.stonybrook.edu/~px/Papers/NR:lifted_tr_2016/
David Poole. First-order probabilistic inference. In Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, volume 3, pages 985-991, 2003.
Fabrizio Riguzzi and Terrance Swift. The PITA system: Tabling and answer subsumption for reasoning under uncertainty. TPLP, 11(4-5):433-449, 2011.
Taisuke Sato and Yoshitaka Kameya. PRISM: a language for symbolic-statistical modeling. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, volume 97, pages 1330-1339, 1997.
Taisuke Sato and Yoshitaka Kameya. Parameter learning of logic programs for symbolic-statistical modeling. Journal of Artificial Intelligence Research, pages 391-454, 2001.
Daniel R Sheldon and Thomas G. Dietterich. Collective graphical models. In Advances in Neural Information Processing Systems 24, pages 1161-1169, 2011. URL: http://papers.nips.cc/paper/4220-collective-graphical-models.pdf.
http://papers.nips.cc/paper/4220-collective-graphical-models.pdf
Arvind Srinivasan, Timothy Kam, Sharad Malik, and Robert K. Brayton. Algorithms for discrete function manipulation. In International Conference on Computer-Aided Design, ICCAD, pages 92-95, 1990. URL: http://dx.doi.org/10.1109/ICCAD.1990.129849.
http://dx.doi.org/10.1109/ICCAD.1990.129849
Nima Taghipour, Daan Fierens, Jesse Davis, and Hendrik Blockeel. Lifted variable elimination: Decoupling the operators from the constraint language. J. Artif. Intell. Res. (JAIR), 47:393-439, 2013.
Guy Van den Broeck, Nima Taghipour, Wannes Meert, Jesse Davis, and Luc De Raedt. Lifted probabilistic inference by first-order knowledge compilation. In IJCAI, pages 2178-2185, 2011.
Sergio Yovine. Model-checking timed automata. In Embedded Systems, number 1494 in LNCS, pages 114-152, 1998.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
On the Expressiveness of Spatial Constraint Systems
In this paper we shall report on our progress using spatial constraint system as an abstract representation of modal and epistemic behaviour. First we shall give an introduction as well as the background to our work. Then, we present our preliminary results on the representation of modal behaviour by using spatial constraint systems. Then, we present our ongoing work on the characterization of the epistemic notion of knowledge. Finally, we discuss about the future work of our research.
Epistemic logic
Modal logic
Constraint systems
Concurrent constraint programming
16:1-16:12
Regular Paper
Michell
Guzmán
Michell Guzmán
Frank D.
Valencia
Frank D. Valencia
10.4230/OASIcs.ICLP.2016.16
Samson Abramsky and Achim Jung. Domain theory. Handbook of logic in computer science, pages 1-77, 1994.
Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal Logic. Cambridge University Press, 1st edition, 2002.
Frank S. Boer, Alessandra Di Pierro, and Catuscia Palamidessi. Nondeterminism and infinite computations in constraint programming. Theoretical Computer Science, pages 37-78, 1995.
Alessandra Di Pierro, Catuscia Palamidessi, and Frank S. Boer. An algebraic perspective of constraint logic programming. Journal of Logic and Computation, pages 1-38, 1997.
Ronald Fagin, Joseph Y Halpern, Yoram Moses, and Moshe Y Vardi. Reasoning about knowledge. MIT press Cambridge, 4th edition, 1995.
M. Guzman, S. Haar, S. Perchy, C. Rueda, and F. Valencia. Belief, knowledge, lies and other utterances in an algebra for space and extrusion. Journal of Logical and Algebraic Methods in Programming, 2016.
M. Guzman, S. Perchy, C. Rueda, and F. Valencia. Deriving extrusion on constraint systems from concurrent constraint programming process calculi. In ICTAC 2016, 2016.
Jaakko Hintikka. Knowledge and belief. Cornell Univeristy Press, 1962.
Sophia Knight, Catuscia Palamidessi, Prakash Panangaden, and Frank D Valencia. Spatial and epistemic modalities in constraint-based process calculi. In CONCUR 2012, pages 317-332. Springer, 2012.
John Charles Chenoweth McKinsey and Alfred Tarski. The algebra of topology. Annals of mathematics, pages 141-191, 1944.
Nax P Mendler, Prakash Panangaden, Philip J Scott, and RAG Seely. A logical view of concurrent constraint programming. Nordic Journal of Computing, pages 181-220, 1995.
Prakash Panangaden, Vijay Saraswat, Philip J Scott, and RAG Seely. A hyperdoctrinal view of concurrent constraint programming. In Workshop of Semantics: Foundations and Applications, REX, pages 457-476. Springer, 1993.
Amir Pnueli and Zohar Manna. The temporal logic of reactive and concurrent systems. Springer, 1992.
Sally Popkorn. First steps in modal logic. Cambridge University Press, 1st edition, 1994.
Vijay A Saraswat, Martin Rinard, and Prakash Panangaden. Semantic foundations of concurrent constraint programming. In POPL'91, pages 333-352, 1991.
Steven Vickers. Topology via logic. Cambridge University Press, 1st edition, 1996.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Tabled CLP for Reasoning Over Stream Data
The interest in reasoning over stream data is growing as quickly as the amount of data generated. Our intention is to change the way stream data is analyzed. This is an important problem because we constantly have new sensors collecting information, new events from electronic devices and/or from customers and we want to reason about this information. For example, information about traffic jams and costumer order could be used to define a deliverer route. When there is a new order or a new traffic jam, we usually restart from scratch in order to recompute the route. However, if we have several deliveries and we analyze the information from thousands of sensors, we would like to reduce the computation requirements, e.g. reusing results from the previous computation. Nowadays, most of the applications that analyze stream data are specialized for specific problems (using complex algorithms and heuristics) and combine a computation language with a query language. As a result, when the problems become more complex (in e.g. reasoning requirements), in order to modify the application complex and error prone coding is required.
We propose a framework based on a high-level language rooted in logic and constraints that will be able to provide customized services to different problems. The framework will discard wrong solutions in early stages and will reuse previous results that are still consistent with the current data set. The use of a constraint logic programming language will make it easier to translate the problem requirements into the code and will minimize the amount of re-engineering needed to comply with the requirements when they change.
logic
languages
tabling
constraints
graph
analysis
reasoning
17:1-17:8
Regular Paper
Joaquín
Arias
Joaquín Arias
10.4230/OASIcs.ICLP.2016.17
James F Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26(11):832-843, 1983.
J. Arias and M. Carro. Description and Evaluation of a Generic Design to Integrate CLP and Tabled Execution. In 18th Int'l. ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming (PPDP'16). ACM Press, September 2016.
Witold Charatonik, Supratik Mukhopadhyay, and Andreas Podelski. Constraint-based infinite model checking and tabulation for stratified clp. In Peter J. Stuckey, editor, ICLP, volume 2401 of Lecture Notes in Computer Science, pages 115-129. Springer, 2002.
P. Chico de Guzmán, M. Carro, M. Hermenegildo, and P. Stuckey. A General Implementation Framework for Tabled CLP. In Tom Schrijvers and Peter Thiemann, editors, FLOPS'12, number 7294 in LNCS, pages 104-119. Springer Verlag, May 2012.
P. Chico de Guzmán, M. Carro, and David S. Warren. Swapping Evaluation: A Memory-Scalable Solution for Answer-On-Demand Tabling. Theory and Practice of Logic Programming, 26th Int'l. Conference on Logic Programming (ICLP'10) Special Issue, 10 (4-6):401-416, July 2010.
Brian Chin, Daniel von Dincklage, Vuk Ercegovac, Peter Hawkins, Mark S Miller, Franz Och, Christopher Olston, and Fernando Pereira. Yedalog: Exploring knowledge at scale. In LIPIcs-Leibniz International Proceedings in Informatics, volume 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015.
Baoqiu Cui and David Scott Warren. A System for Tabled Constraint Logic Programming. In Computational Logic, pages 478-492, 2000.
S. Dawson, C. R. Ramakrishnan, and D. S. Warren. Practical Program Analysis Using General Purpose Logic Programming Systems - A Case Study. In Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation, pages 117-126, New York, USA, 1996. ACM Press.
Deductive Application Language System. URL: http://wis.cs.ucla.edu/deals/.
http://wis.cs.ucla.edu/deals/
Juliana Freire, Terrance Swift, and David Scott Warren. Beyond Depth-First Strategies: Improving Tabled Logic Programs through Alternative Scheduling. Journal of Functional and Logic Programming, 1998(3), 1998.
Todd J Green, Dan Olteanu, and Geoffrey Washburn. Live programming in the LogicBlox system: a MetaLogiQL approach. Proceedings of the VLDB Endowment, 8(12):1782-1791, 2015.
J. Jaffar and M.J. Maher. Constraint LP: A Survey. JLP, 19/20:503-581, 1994.
Paris C. Kanellakis, Gabriel M. Kuper, and Peter Z. Revesz. Constraint Query Languages. J. Comput. Syst. Sci., 51(1):26-52, 1995.
David B Kemp and Peter J Stuckey. Semantics of logic programs with aggregates. In ISLP, volume 91, pages 387-401. Citeseer, 1991.
Pei Lee, Laks VS Lakshmanan, and Evangelos E Milios. Incremental cluster evolution tracking from highly dynamic network data. In 2014 IEEE 30th International Conference on Data Engineering, pages 3-14. IEEE, 2014.
OWL Web Ontology Language Guide. URL: http://www.w3.org/TR/owl-guide/.
http://www.w3.org/TR/owl-guide/
Emanuele Panigati, Fabio A Schreiber, and Carlo Zaniolo. Data streams and data stream management systems and languages. In Data Management in Pervasive Systems, pages 93-111. Springer International Publishing, 2015.
Nikolay Pelov, Marc Denecker, and Maurice Bruynooghe. Well-Founded and Stable Semantics of Logic Programs with Aggregates. TPLP, 7(3):301-353, 2007. URL: http://dx.doi.org/10.1017/S1471068406002973.
http://dx.doi.org/10.1017/S1471068406002973
Protocol Buffers. URL: https://developers.google.com/protocol-buffers/.
https://developers.google.com/protocol-buffers/
Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, S.A. Smolka, T. Swift, and D.S. Warren. Efficient Model Checking Using Tabled Resolution. In CAV, volume 1254 of LNCS, pages 143-154. Springer Verlag, 1997.
Resource Description Framework (RDF). URL: https://www.w3.org/RDF/.
https://www.w3.org/RDF/
Konstantinos F. Sagonas and Peter J. Stuckey. Just Enough Tabling. In Principles and Practice of Declarative Programming, pages 78-89. ACM, August 2004.
Tom Schrijvers, Bart Demoen, and David Scott Warren. TCHR: a Framework for Tabled CLP. TPLP, 8(4):491-526, 2008.
Terrance Swift. Incremental tabling in support of knowledge representation and reasoning. Theory and Practice of Logic Programming, 14(4-5):553-567, 2014.
Terrance Swift and David Scott Warren. Tabling with answer subsumption: Implementation, applications and performance. In Tomi Janhunen and Ilkka Niemelä, editors, JELIA, volume 6341 of Lecture Notes in Computer Science, pages 300-312. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15675-5.
http://dx.doi.org/10.1007/978-3-642-15675-5
H. Tamaki and M. Sato. OLD Resol. with Tabulation. In ICLP, pages 84-98. LNCS, 1986.
David Toman. Constraint Databases and Program Analysis Using Abstract Interpretation. In CDTA, volume 1191 of LNCS, pages 246-262, 1997.
David Toman. Memoing Evaluation for Constraint Extensions of Datalog. Constraints, 2(3/4):337-359, 1997. URL: http://dx.doi.org/10.1023/A:1009799613661.
http://dx.doi.org/10.1023/A:1009799613661
Alexander Vandenbroucke, Maciej Pirog, Benoit Desouter, and Tom Schrijvers. Tabling with Sound Answer Subsumption. Theory and Practice of Logic Programming, 32th Int'l. Conference on Logic Programming (ICLP'16), 16, October 2016.
D. S. Warren. Memoing for Logic Programs. CACM, 35(3):93-111, 1992.
R. Warren, M. Hermenegildo, and S. K. Debray. On the Practicality of Global Flow Analysis of Logic Programs. In JICSLP, pages 684-699. MIT Press, August 1988.
Peter T Wood. Query languages for graph databases. ACM SIGMOD Record, 41(1):50-60, 2012.
Carlo Zaniolo. A logic-based language for data streams. In SEBD, pages 59-66, 2012.
Youyong Zou, Tim Finin, and Harry Chen. F-OWL: An Inference Engine for Semantic Web. In Formal Approaches to Agent-Based Systems, volume 3228 of Lecture Notes in Computer Science, pages 238-248. Springer Verlag, January 2005.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Testing of Concurrent Programs
Testing concurrent systems requires exploring all possible non-deterministic interleavings that the concurrent execution may have, as any of the interleavings may reveal erroneous behaviour. This introduces a new problem: the well-known state space problem, which is often computationally intractable. In the present thesis, this issue will be addressed through: (1) the development of new Partial-Order Reduction Techniques and (2) the combination of static analysis and testing (property-based testing) in order to reduce the combinatorial explosion. As a preliminary result, we have performed an experimental evaluation on the SYCO tool, a CLP-based testing framework for actor-based concurrency, where these techniques have been implemented. Finally, our experiments prove the effectiveness and applicability of the proposed techniques.
Property-based Testing
Partial Order Reduction
Deadlock-Guided Testing
Deadlock Detection
Systematic Testing
18:1-18:5
Regular Paper
Miguel
Isabel
Miguel Isabel
10.4230/OASIcs.ICLP.2016.18
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Controlled Natural Languages for Knowledge Representation and Reasoning
Controlled natural languages (CNLs) are effective languages for knowledge representation and reasoning. They are designed based on certain natural languages with restricted lexicon and grammar. CNLs are unambiguous and simple as opposed to their base languages. They preserve the expressiveness and coherence of natural languages. In this paper, it mainly focuses on a class of CNLs, called machine-oriented CNLs, which have well-defined semantics that can be deterministically translated into formal languages to do logical reasoning. Although a number of machine-oriented CNLs emerged and have been used in many application domains for problem solving and question answering, there are still many limitations: First, CNLs cannot handle inconsistencies in the knowledge base. Second, CNLs are not powerful enough to identify different variations of a sentence and therefore might not return the expected inference results. Third, CNLs do not have a good mechanism for defeasible reasoning. This paper addresses these three problems and proposes a research plan for solving these problems. It also shows the current state of research: a paraconsistent logical framework from which six principles that guide the user to encode CNL sentences were created. Experiment results show this paraconsistent logical framework and these six principles can consistently and effectively solve word puzzles with injections of inconsistencies.
Controlled Natural Languages
Paraconsistent Logics
Defeasible Reasoning
19:1-19:10
Regular Paper
Tiantian
Gao
Tiantian Gao
10.4230/OASIcs.ICLP.2016.19
Gabor Angeli, Melvin Jose Johnson Premkumar, and Christopher D. Manning. Leveraging linguistic structure for open domain information extraction. In Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language Processing of the Asian Federation of Natural Language Processing, ACL 2015, July 26-31, 2015, Beijing, China, Volume 1: Long Papers, pages 344-354. Association for Computational Linguistics, The Association for Computer Linguistics, 2015.
Marcello Balduccini. Representing constraint satisfaction problems in answer set programming. In ICLP09 Workshop on Answer Set Programming and Other Computing Paradigms (ASPOCP09)(Jul 2009), 2009.
Marcello Balduccini. A "conservative" approach to extending answer set programming with non-herbrand functions. In Correct Reasoning, pages 24-39. Springer, 2012.
Marcello Balduccini. Asp with non-herbrand partial functions: A language and system for practical use. Theory and Practice of Logic Programming, 13(4-5):547-561, 2013.
Marcello Balduccini and Michael Gelfond. Logic programs with consistency-restoring rules. In International Symposium on Logical Formalization of Commonsense Reasoning, AAAI 2003 Spring Symposium Series, volume 102, 2003.
Chitta Baral, Juraj Dzifcak, Marcos Alvarez Gonzalez, and Aaron Gottesman. Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them. TPLP, 12(4-5):775-791, 2012.
Chitta Baral, Juraj Dzifcak, Marcos Alvarez Gonzalez, and Jiayu Zhou. Using inverse lambda and generalization to translate english to formal languages. CoRR, abs/1108.3843, 2011.
Ken Barker, Bruce W. Porter, and Peter Clark. A library of generic concepts for composing knowledge bases. In Proceedings of the First International Conference on Knowledge Capture (K-CAP 2001), October 21-23, 2001, Victoria, BC, Canada, pages 14-21. ACM, 2001.
Nuel D Belnap Jr. A useful four-valued logic. In Modern uses of multiple-valued logic, pages 5-37. Springer, 1977.
Jean-Yves Béziau, Walter Alexandre Carnielli, and Dov M Gabbay. Handbook of paraconsistency. College Publications, 2007.
Howard A Blair and VS Subrahmanian. Paraconsistent logic programming. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 340-360. Springer, 1987.
Gerhard Brewka, James P. Delgrande, Javier Romero, and Torsten Schaub. asprin: Customizing answer set preferences without a headache. In Blai Bonet and Sven Koenig, editors, Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA., pages 1467-1474. AAAI Press, 2015.
Peter Clark, Shaw Yi Chaw, Ken Barker, Vinay K. Chaudhri, Philip Harrison, James Fan, Bonnie E. John, Bruce W. Porter, Aaron Spaulding, John A. Thompson, and Peter Z. Yeh. Capturing and answering questions posed to a knowledge-based system. In Derek H. Sleeman and Ken Barker, editors, Proceedings of the 4th International Conference on Knowledge Capture (K-CAP 2007), October 28-31, 2007, Whistler, BC, Canada, pages 63-70. ACM, 2007.
Peter Clark, Philip Harrison, Thomas Jenkins, John A. Thompson, and Richard H. Wojcik. Acquiring and using world knowledge using a restricted subset of english. In Ingrid Russell and Zdravko Markov, editors, Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, Clearwater Beach, Florida, USA, pages 506-511. AAAI Press, 2005.
Peter Clark, Bruce Porter, and Boeing Phantom Works. Km?the knowledge machine 2.0: Users manual. Department of Computer Science, University of Texas at Austin, 2:5, 2004.
Esra Erdem, Halit Erdogan, and Umut Öztok. BIOQUERY-ASP: querying biomedical ontologies using answer set programming. In Stefano Bragaglia, Carlos Viegas Damásio, Marco Montali, Alun D. Preece, Charles J. Petrie, Mark Proctor, and Umberto Straccia, editors, Proceedings of the 5th International RuleML2011@BRF Challenge, co-located with the 5th International Rule Symposium, Fort Lauderdale, Florida, USA, November 3-5, 2011, volume 799 of CEUR Workshop Proceedings. CEUR-WS.org, 2011.
Norbert E. Fuchs, Kaarel Kaljurand, and Tobias Kuhn. Attempto controlled english for knowledge representation. In Cristina Baroglio, Piero A. Bonatti, Jan Maluszynski, Massimo Marchiori, Axel Polleres, and Sebastian Schaffert, editors, Reasoning Web, 4th International Summer School 2008, Venice, Italy, September 7-11, 2008, Tutorial Lectures, volume 5224 of Lecture Notes in Computer Science, pages 104-124. Springer, 2008.
Norbert E. Fuchs, Kaarel Kaljurand, and Tobias Kuhn. Discourse Representation Structures for ACE 6.6. Technical Report ifi-2010.0010, Department of Informatics, University of Zurich, Zurich, Switzerland, 2010.
Norbert E. Fuchs and Uta Schwertel. Reasoning in attempto controlled english. In François Bry, Nicola Henze, and Jan Maluszynski, editors, Principles and Practice of Semantic Web Reasoning, International Workshop, PPSWR 2003, Mumbai, India, December 8, 2003, Proceedings, volume 2901 of Lecture Notes in Computer Science, pages 174-188. Springer, 2003.
Tiantian Gao, Paul Fodor, and Michael Kifer. Paraconsistency and word puzzles. CoRR, abs/1608.01338, 2016.
Martin Gebser, Benjamin Kaufmann, Roland Kaminski, Max Ostrowski, Torsten Schaub, and Marius Thomas Schneider. Potassco: The potsdam answer set solving collection. AI Commun., 24(2):107-124, 2011.
Michael Gelfond and Yulia Kahl. Knowledge representation, reasoning, and the design of intelligent agents: The answer-set programming approach. Cambridge University Press, 2014.
ASD Simplified Technical English Maintenance Group. ASD-STE 100: Simplified Technical English : International Specification for the Preparation of Maintenance Documentation in a Controlled Language. Aerospace and Defence Industries Association of Europe, 2007.
Philip Harrison and Michael Maxwell. A new implementation of gpsg. In Proc. 6th Canadian Conf on AI, pages 78-83, 1986.
Hans Kamp and Uwe Reyle. From discourse to logic: Introduction to modeltheoretic semantics of natural language, formal logic and discourse representation theory, volume 42. Springer Science &Business Media, 2013.
Michael Kifer and Eliezer L. Lozinskii. A logic for reasoning with inconsistency. J. Autom. Reasoning, 9(2):179-215, 1992.
Tobias Kuhn. A survey and classification of controlled natural languages. Computational Linguistics, 40(1):121-170, 2014.
Tom Kwiatkowski, Luke S. Zettlemoyer, Sharon Goldwater, and Mark Steedman. Inducing probabilistic CCG grammars from logical form with higher-order unification. In Proceedings of the 2010 Conference on Empirical Methods in Natural Language Processing, EMNLP 2010, 9-11 October 2010, MIT Stata Center, Massachusetts, USA, A meeting of SIGDAT, a Special Interest Group of the ACL, pages 1223-1233. ACL, 2010.
Vladimir Lifschitz. Closed-world databases and circumscription. Artif. Intell., 27(2):229-235, 1985.
Rainer Manthey and François Bry. Satchmo: a theorem prover implemented in prolog. In International Conference on Automated Deduction, pages 415-434. Springer, 1988.
Mausam, Michael Schmitz, Stephen Soderland, Robert Bart, and Oren Etzioni. Open language learning for information extraction. In Jun'ichi Tsujii, James Henderson, and Marius Pasca, editors, Proceedings of the 2012 Joint Conference on Empirical Methods in Natural Language Processing and Computational Natural Language Learning, EMNLP-CoNLL 2012, July 12-14, 2012, Jeju Island, Korea, pages 523-534. ACL, 2012.
William McCune. Otter 3.0 reference manual and guide, volume 9700. Argonne National Laboratory Argonne, IL, 1994.
William McCune. Mace4 reference manual and guide. arXiv preprint cs/0310055, 2003.
Donald Nute. Defeasible logic, handbook of logic in artificial intelligence and logic programming (vol. 3): nonmonotonic reasoning and uncertain reasoning, 1994.
Voice of America (Organization). VOA Special English word book: a list of words used in Special English programs on radio, television, and the Internet. Voice of America, 2007.
Charles Kay Ogden. Basic English: A general introduction with rules and grammar. Number 29 in Psyche miniatures., General series. K. Paul, Trench, Trubner, 1944.
Graham Priest, Koji Tanaka, and Zach Weber. Paraconsistent logic. München, 1989.
Teodor C. Przymusinski. Well-founded and stationary models of logic programs. Ann. Math. Artif. Intell., 12(3-4):141-187, 1994.
Rolf Schwitter. English as a formal specification language. In 13th International Workshop on Database and Expert Systems Applications (DEXA 2002), 2-6 September 2002, Aix-en-Provence, France, pages 228-232. IEEE Computer Society, 2002.
Rolf Schwitter. Controlled natural languages for knowledge representation. In Chu-Ren Huang and Dan Jurafsky, editors, COLING 2010, 23rd International Conference on Computational Linguistics, Posters Volume, 23-27 August 2010, Beijing, China, pages 1113-1121. Chinese Information Processing Society of China, 2010.
Rolf Schwitter. The jobs puzzle: Taking on the challenge via controlled natural language processing. TPLP, 13(4-5):487-501, 2013.
Rolf Schwitter. Working with defaults in a controlled natural language. In Australasian Language Technology Association Workshop 2013, page 106, 2013.
Nguyen H Vo, Arindam Mitra, and Chitta Baral. The nl2kr platform for building natural language translation systems. In Association for Computational Linguistics (ACL), 2015.
Hui Wan, Benjamin N. Grosof, Michael Kifer, Paul Fodor, and Senlin Liang. Logic programming with defaults and argumentation theories. In Patricia M. Hill and David Scott Warren, editors, Logic Programming, 25th International Conference, ICLP 2009, Pasadena, CA, USA, July 14-17, 2009. Proceedings, volume 5649 of Lecture Notes in Computer Science, pages 432-448. Springer, 2009.
L. Wos. Automated reasoning: introduction and applications. McGraw-Hill, 1992.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
The Functional Perspective on Advanced Logic Programming
The basics of logic programming, as embodied by Prolog, are generally well-known in the programming language community. However, more advanced techniques, such as tabling, answer subsumption and probabilistic logic programming fail to attract the attention of a larger audience. The cause for the community's seemingly limited interest lies with the presentation of these features: the literature frequently focuses on implementations and examples that do little to aid the understanding of non-experts in the field. The key point is that many of these advanced logic programming features can be characterised in more generally known, more accessible terms. In my research I try to reconcile these advanced concepts from logic programming (Tabling, Answer subsumption and probabilistic programming) with concepts from functional programming (effects, monads and applicative functors).
Tabling
Answer Subsumption
Effect Handlers
Functional Programming
Logic Programming
Probabilistic Programming
20:1-20:8
Regular Paper
Alexander
Vandenbroucke
Alexander Vandenbroucke
10.4230/OASIcs.ICLP.2016.20
Samson Abramsky and Chris Hankin. Abstract Interpretation of declarative languages, volume 1, chapter An introduction to abstract interpretation, pages 63-102. 1987.
Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. ProbLog: A probabilistic prolog and its application in link discovery. In IJCAI, volume 7, pages 2462-2467, 2007.
Benoit Desouter, Marko van Dooren, and Tom Schrijvers. Tabling as a library with delimited control. TPLP, 15(4-5):419-433, 2015. URL: http://dx.doi.org/10.1017/S1471068415000137.
http://dx.doi.org/10.1017/S1471068415000137
Jeremy Gibbons and Ralf Hinze. Just do it: simple monadic equational reasoning. In ICFP, pages 2-14. ACM, 2011.
Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. Church: a language for generative models. In UAI, pages 220-229. AUAI Press, 2008.
Hai-Feng Guo and Gopal Gupta. Simplifying dynamic programming via tabling. In PADL, volume 3057 of LNCS, pages 163-177. Springer, 2004.
Oleg Kiselyov, Amr Sabry, and Cameron Swords. Extensible effects: an alternative to monad transformers. In Haskell, pages 59-70. ACM, 2013.
Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of probabilistic real-time systems. In CAV, volume 6806, pages 585-591. Springer, 2011.
Conor McBride and Ross Paterson. Applicative programming with effects. JFP, 18(1):1-13, 2008.
Andrew McCallum, Karl Schultz, and Sameer Singh. FACTORIE: probabilistic programming via imperatively defined factor graphs. In NIPS, pages 1249-1257. Curran Associates, Inc., 2009.
Microsoft Research. Infer.NET. URL: http://research.microsoft.com/en-us/um/cambridge/projects/infernet/.
http://research.microsoft.com/en-us/um/cambridge/projects/infernet/
Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991.
Avi Pfeffer. Figaro: An object-oriented probabilistic programming language. Charles River Analytics Technical Report, 137, 2009.
Norman Ramsey and Avi Pfeffer. Stochastic lambda calculus and monads of probability distributions. In POPL, pages 154-165. ACM, 2002.
Amr Hany Saleh. Transforming delimited control: Achieving faster effect handlers. In ICLP (Technical Communications), volume 1433 of CEUR Workshop Proceedings. CEUR-WS.org, 2015.
Vítor Santos Costa, Ricardo Rocha, and Luís Damas. The YAP Prolog system. TPLP, 12(1-2):5-34, 2012.
Adam Ścibior, Zoubin Ghahramani, and Andrew D Gordon. Practical probabilistic programming with monads. In Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, pages 165-176. ACM, 2015.
Terrance Swift and David S. Warren. Tabling with answer subsumption: Implementation, applications and performance. In LAI, volume 6341 of LNCS, pages 300-312. Springer, 2010.
Terrance Swift and David S. Warren. XSB: Extending Prolog with tabled logic programming. TPLP, 12(1-2):157-187, January 2012.
Alexander Vandenbroucke, Maciej Piróg, Benoit Desouter, and Tom Schrijvers. Tabling with sound answer subsumption. arXiv preprint arXiv:1608.00787, 2016.
Alexander Vandenbroucke, Tom Schrijvers, and Frank Piessens. Fixing non-determinism. In IFL 2015: Symposium on the implementation and application of functional programming languages Proceedings. Association for Computing Machinery, 2016.
Philip Wadler. Monads for functional programming. In Advanced Functional Programming, volume 925 of Lecture Notes in Computer Science, pages 24-52. Springer, 1995.
David S. Warren. Programming in Tabled Prolog, 1999. URL: http://www3.cs.stonybrook.edu/~warren/xsbbook/.
http://www3.cs.stonybrook.edu/~warren/xsbbook/
Jan Wielemaker, S Ss, and I Ii. Swi-prolog 2.7-reference manual, 1996.
Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. A new approach to probabilistic programming inference. In Proceedings of the 17th International conference on Artificial Intelligence and Statistics, pages 1024-1032, 2014.
Neng-Fa Zhou. The language features and architecture of B-Prolog. TPLP, 12(1-2):189-218, 2012.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Methods for Solving Extremal Problems in Practice
During the 20 th century there has been an incredible progress in solving theoretically hard problems in practice. One of the most prominent examples is the DPLL algorithm and its derivatives to solve the Boolean satisfiability problem, which can handle instances with millions of variables and clauses in reasonable time, notwithstanding the theoretical difficulty of solving the problem.
Despite this progress, there are classes of problems that contain especially hard instances, which have remained open for decades despite their relative small size. One such class is the class of extremal problems, which typically involve finding a combinatorial object under some constraints (e.g, the search for Ramsey numbers). In recent years, a number of specialized methods have emerged to tackle extremal problems. Most of these methods are applied to a specific problem, despite the fact there is a great deal in common between different problems.
Following a meticulous examination of these methods, we would like to extend them to handle general extremal problems. Further more, we would like to offer ways to exploit the general structure of extremal problems in order to develop constraints and symmetry breaking techniques which will, hopefully, improve existing tools. The latter point is of immense importance in the context of extremal problems, which often hamper existing tools when there is a great deal of symmetry in the search space, or when not enough is known of the problem structure. For example, if a graph is a solution to a problem instance, in many cases any isomorphic graph will also be a solution. In such cases, existing methods can usually be applied only if the model excludes symmetries.
Extremal Problems
Constraints
SAT Solving
Logic Programming
Parallelism
21:1-21:6
Regular Paper
Michael
Frank
Michael Frank
10.4230/OASIcs.ICLP.2016.21
Joan Boyar and René Peralta. Tight bounds for the multiplicative complexity of symmetric functions. TCS, 396(1-3):223-246, 2008.
Joan Boyar, René Peralta, and Denis Pochuev. On the multiplicative complexity of Boolean functions over the basis (∧, +, 1). TCS, 235(1):43-57, 2000.
Daniel Bundala and Jakub Zavodny. Optimal sorting networks. In Adrian Horia Dediu, Carlos Martín-Vide, José Luis Sierra-Rodríguez, and Bianca Truthe, editors, Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, volume 8370 of Lecture Notes in Computer Science, pages 236-247. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-04921-2_19.
http://dx.doi.org/10.1007/978-3-319-04921-2_19
Michael Codish, Luís Cruz-Filipe, Michael Frank, and Peter Schneider-Kamp. When six gates are not enough. CoRR, abs/1508.05737, 2015. URL: http://arxiv.org/abs/1508.05737.
http://arxiv.org/abs/1508.05737
Michael Codish, Luís Cruz-Filipe, Michael Frank, and Peter Schneider-Kamp. Sorting nine inputs requires twenty-five comparisons. Journal of Computer and System Sciences, 82(3):551-563, 2016. URL: http://dx.doi.org/10.1016/j.jcss.2005.06.002.
http://dx.doi.org/10.1016/j.jcss.2005.06.002
Michael Codish, Michael Frank, Avraham Itzhakov, and Alice Miller. Computing the ramsey number r(4, 3, 3) using abstraction and symmetry breaking. CoRR, abs/1510.08266, 2015. URL: http://arxiv.org/abs/1510.08266.
http://arxiv.org/abs/1510.08266
Michael Codish, Alice Miller, Patrick Prosser, and Peter James Stuckey. Breaking symmetries in graph representation. In Francesca Rossi, editor, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China. IJCAI/AAAI, 2013. URL: http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6480.
http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6480
Thomas H. Cormen, Clifford Stein, Ronald L. Rivest, and Charles E. Leiserson. Introduction to Algorithms. McGraw-Hill Higher Education, 2nd edition, 2001.
Niklas Eén and Niklas Sörensson. Minisat sat solver. URL: http://minisat.se/Main.html.
http://minisat.se/Main.html
Thorsten Ehlers and Mike Müller. Faster sorting networks for 17, 19 and 20 inputs. CoRR, abs/1410.2736, 2014. URL: http://arxiv.org/abs/1410.2736.
http://arxiv.org/abs/1410.2736
Thorsten Ehlers and Mike Müller. New bounds on optimal sorting networks. CoRR, abs/1501.06946, 2015. URL: http://arxiv.org/abs/1501.06946.
http://arxiv.org/abs/1501.06946
M. Frank and M. Codish. Logic programming with graph automorphism: Integrating nauty with prolog (a tool paper). Technical report, Department of Computer Science, Ben-Gurion University of the Negev, Beer-Sheva, Israel, 2016. URL: https://www.cs.bgu.ac.il/~frankm/plnauty/.
https://www.cs.bgu.ac.il/~frankm/plnauty/
Hiroshi Fujita. A new lower bound for the ramsey number r(4, 8). CoRR, abs/1212.1328, 2012. URL: http://arxiv.org/abs/1212.1328.
http://arxiv.org/abs/1212.1328
M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub, and M. Schneider. Potassco: The Potsdam answer set solving collection. AI Communications, 24(2):107-124, 2011.
Avraham Itzhakov and Michael Codish. Breaking symmetries in graph search with canonizing sets. CoRR, abs/1511.08205, 2015. URL: http://arxiv.org/abs/1511.08205.
http://arxiv.org/abs/1511.08205
Donald E. Knuth. The Art of Computer Programming, Volume 3: (2Nd Ed.) Sorting and Searching. Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, USA, 1998.
B. McKay. nauty user’s guide (version 1.5). Technical Report TR-CS-90-02, Australian National University, Computer Science Department, 1990.
Brendan D. McKay and Stanislaw P. Radziszowski. R(4, 5) = 25. Journal of Graph Theory, 19(3):309-322, 1995. URL: http://dx.doi.org/10.1002/jgt.3190190304.
http://dx.doi.org/10.1002/jgt.3190190304
Amit Metodi and Michael Codish. Compiling finite domain constraints to sat with bee. Theory and Practice of Logic Programming, 12(4-5):465-483, 2012.
Amit Metodi, Michael Codish, and Peter J. Stuckey. Boolean equi-propagation for concise and efficient SAT encodings of combinatorial problems. J. Artif. Intell. Res. (JAIR), 46:303-341, 2013. URL: http://dx.doi.org/10.1613/jair.3809.
http://dx.doi.org/10.1613/jair.3809
Stanislaw P. Radziszowski. Small Ramsey numbers. Electronic Journal of Combinatorics, 1994. Revision #14: January, 2014. URL: http://www.combinatorics.org/.
http://www.combinatorics.org/
Mate Soos. CryptoMiniSAT, v2.5.1, 2010. URL: http://www.msoos.org/cryptominisat2.
http://www.msoos.org/cryptominisat2
Meltem Sönmez Turan and René Peralta. The multiplicative complexity of Boolean functions on four and five variables. In Thomas Eisenbarth and Erdinç Öztürk, editors, LightSec 2014, volume 8898 of LNCS, pages 21-33. Springer, 2015.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Automating Disease Management Using Answer Set Programming
Management of chronic diseases such as heart failure, diabetes, and chronic obstructive pulmonary disease (COPD) is a major problem in health care. A standard approach that the medical community has devised to manage widely prevalent chronic diseases such as chronic heart failure (CHF) is to have a committee of experts develop guidelines that all physicians should follow. These guidelines typically consist of a series of complex rules that make recommendations based on a patient's information. Due to their complexity, often the guidelines are either ignored or not complied with at all, which can result in poor medical practices. It is not even clear whether it is humanly possible to follow these guidelines due to their length and complexity. In the case of CHF management, the guidelines run nearly 80 pages. In this paper we describe a physician-advisory system for CHF management that codes the entire set of clinical practice guidelines for CHF using answer set programming. Our approach is based on developing reasoning templates (that we call knowledge patterns) and using these patterns to systemically code the clinical guidelines for CHF as ASP rules. Use of the knowledge patterns greatly facilitates the development of our system. Given a patient's medical information, our system generates a recommendation for treatment just as a human physician would, using the guidelines. Our system will work even in the presence of incomplete information. Our work makes two contributions: (i) it shows that highly complex guidelines can be successfully coded as ASP rules, and (ii) it develops a series of knowledge patterns that facilitate the coding of knowledge expressed in a natural language and that can be used for other application domains.
chronic disease management
knowledge pattern
answer set programming
knowledge representation
automated reasoning
22:1-22:10
Regular Paper
Zhuo
Chen
Zhuo Chen
10.4230/OASIcs.ICLP.2016.22
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode
Scalable Design Space Exploration via Answer Set Programming
The design of embedded systems is becoming continuously more complex such that the application of efficient high level design methods are crucial for competitive results regarding design time and performance. Recently, advances in Boolean constraint solvers for Answer Set Programming (ASP) allow for easy integration of background theories and more control over the solving process. The goal of this research is to leverage those advances for system level design space exploration while using specialized techniques from electronic design automation that drive new application-originated ideas for multi-objective combinatorial optimization.
Answer Set Programming
System Synthesis
Multi-Objective Optimization
23:1-23:11
Regular Paper
Philipp
Wanko
Philipp Wanko
10.4230/OASIcs.ICLP.2016.23
Santosh G. Abraham, B. Ramakrishna Rau, and Robert Schreiber. Fast Design Space Exploration Through Validity and Quality Filtering of Subsystem Designs. Technical report, Hewlett Packard, Compiler and Architecture Research, HP Laboratories Palo Alto, July 2000.
B. Andres, M. Gebser, M. Glaß, C. Haubelt, F. Reimann, and T. Schaub. A combined mapping and routing algorithm for 3D NoCs based on ASP. In C. Haubelt and D. Timmermann, editors, Sechzehnter Workshop für Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV'13), pages 35-46. Institut für Angewandte Mikroelektronik und Datentechnik, Universität Rostock, 2013.
B. Andres, M. Gebser, M. Glaß, C. Haubelt, F. Reimann, and T. Schaub. Symbolic system synthesis using answer set programming. In P. Cabalar and T. Son, editors, Proceedings of the Twelfth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'13), volume 8148 of Lecture Notes in Artificial Intelligence, pages 79-91. Springer, 2013.
C. Baral. Knowledge Representation, Reasoning and Declarative Problem Solving. Cambridge University Press, 2003.
T. Basten, M. Hendriks, L. Somers, and N. Trcka. Model-Driven Design-Space Exploration for Software-Intensive Embedded Systems. In Proceedings of the International Conference on Formal Modeling and Analysis of Timed Systmes (FORMATS), pages 1-6, 2012.
J. F. Benders. Partitioning Procedures for Solving Mixed-Variables Programming Problems. Numerische Mathemathik, 4(3):238-252, 1962.
S. Bhattacharyya, G. Brebner, J. Janneck, J. Eker, C. von Platen, M. Mattavelli, and M. Raulet. OpenDF: A Dataflow Toolset for Reconfigurable Hardware and Multicore Systems. ACM SIGARCH Computer Architecture News, 36(5):29-35, 2009.
A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009.
T. Blickle, J. Teich, and L. Thiele. System-Level Synthesis Using Evolutionary Algorithms. In Design Automation for Embedded Systems, 3, pages 23-62. 1998.
J. R. Burch and D. L. Dill. Automatic Verification of Pipelined Microprocessor Control. In Proceedings of the International Conference on Computer Aided Verification (CAV), pages 68-80, 1994.
K. Deb. Multi-Objective Optimization using Evolutionary Algorithms. John Wiley &Sons, Inc., Chichester, New York, Weinheim, Brisbane, Singapore, Toronto, 2001.
M. Gebser, B. Kaufmann, A. Neumann, and T. Schaub. Conflict-driven answer set enumeration. In C. Baral, G. Brewka, and J. Schlipf, editors, Proceedings of the Ninth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'07), volume 4483 of Lecture Notes in Artificial Intelligence, pages 136-148. Springer, 2007.
M. Geilen and S. Stuijk. Worst-Case Performance Analysis of Synchronous Dataflow Scenarios. In Proceedings of the Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pages 125-134, 2010.
A. Gerstlauer, C. Haubelt, A. D. Pimentel, T. P. Stefanov, D. D. Gajski, and J. Teich. Electronic System-Level Synthesis Methodologies. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 28(10):1517-1530, 2009.
A. H. Ghamarian, M. C. W. Geilen, S. Stuijk, T. Basten, A. J. M. Moonen, M. J. G. Bekooij, B. D. Theelen, and M. R. Mousavi. Throughput Analysis of Synchronous Data Flow Graphs. In Proceedings of the International Conference on Application of Concurrency to System Design (ACSD), pages 25-36, 2006.
A. H. Ghamarian, S. Stuijk, T. Basten, M. C. W. Geilen, and B. D. Theelen. Latency Minimization for Synchronous Data Flow Graphs. In Proceedings of the Euromicro Conference on Digital System Design Architectures, Methods and Tools (DSD), pages 189-196, 2007.
M. Gries. Methods for Evaluating and Covering the Design Space during Early Design Development. Integration, The VLSI Journal, 38(2):131-183, 2004.
S. Gunawan, Ali Farhang-Mehr, and Shapour Azarm. Multi-Level Multi-Objective Genetic Algorithm Using Entropy to Preserve Diversity. In Proceedings of the International Conference on Evolutionary Multi-Criterion Optimization (EMO), pages 148-161, 2003.
W. Haid, M. Keller, K. Huang, I. Bacivarov, and L. Thiele. Generation and Calibration of Compositional Performance Analysis Models for Multi-Processor Systems. In Proceedings of the International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation (SAMOS), pages 92-99, 2009.
C. Haubelt, J. Teich, R. Feldmann, and B. Monien. SAT-Based Techniques in System Design. In Proceedings of the Design, Automation and Test in Europe (DATE), pages 1168-1169, 2003.
J. N. Hooker and G. Ottosson. Logic-Based Benders Decomposition. Mathematical Programming, 96(1):33-60, 2003.
E. Jackson, E. Kang, M. Dahlweid, D. Seifert, and T. Santen. Components, Platforms and Possibilities: Towards Generic Automation for MDA. In Proceedings of the International Conference on Embedded Software (EMSOFT), pages 39-48, 2010.
J. Keinert, M. Streubühr, T. Schlichter, J. Falk, J. Gladigau, C. Haubelt, J. Teich, and M. Meredith. SystemCoDesigner - An Automatic ESL Synthesis Approach by Design Space Exploration and Behavioral Synthesis for Streaming Applications. ACM Transactions on Design Automation of Electronic Systems (TODAES), 14(1):1-23, 2009.
B. Kienhuis, E. Deprettere, K. Vissers, and P. van der Wolf. An Approach for Quantitative Analysis of Application-Specific Dataflow Architectures. In Proceedings of the Conference on Application-Specific Systems, Architectures and Processors (ASAP), pages 338-349, 1997.
R. Kiesel, M. Streubühr, C. Haubelt, O. Löhlein, and J. Teich. Calibration and Validation of Software Performance Models for Pedestrian Detection Systems. In Proceedings of the International Conference on Embedded Computer Systems: Architectures, Modeling and Simulation (SAMOS), pages 182-189, 2011.
P. Kumar, D. B. Chokshi, and L. Thiele. A Satisfiability Approach to Speed Assignment for Distributed Real-Time Systems. In Proceedings of the Design, Automation and Test in Europe (DATE), pages 749-754, 2013.
M. Laumanns, L. Thiele, K. Deb, and E. Zitzler. Combining Convergence and Diversity in Evolutionary Multi-Objective Optimization. Evolutionary Computation, 10(3):263-282, 2002.
C. Li and F. Manyà. MaxSAT. In Biere et al. [8], chapter 19, pages 613-631.
V. Lifschitz and A. Razborov. Why are there so many loop formulas? ACM Transactions on Computational Logic, 7(2):261-268, 2006.
W. Liu, Z. Gu, J. Xu, X. Wu, and Y. Ye. Satisfiability Modulo Graph Theory for Task Mapping and Scheduling on Multiprocessor Systems. IEEE Transactions on Parallel and Distributed Systems, 22(8):1382-1389, 2011.
M. Lukasiewycz, M. Glaß, C. Haubelt, and J. Teich. SAT-Decoding in Evolutionary Algorithms for Discrete Constrained Optimization Problems. In Proceedings of the Congress on Evolutionary Computation, pages 935-942, 2007.
M. Lukasiewycz, M. Glaß, C. Haubelt, and J. Teich. Efficient Symbolic Multi-Objective Design Space Exploration. In Proceedings of the Asia and South Pacific Design Automation Conference (ASPDAC), pages 691-696, 2008.
S. Neema. System Level Synthesis of Adaptive Computing Systems. PhD thesis, Vanderbilt University, Nashville, Tennessee, 2001.
R. Niemann and P. Marwedel. An Algorithm for Hardware/Software Partitioning Using Mixed Integer Linear Programming. Design Automation for Embedded Systems, 2(2):165-193, 1997.
H. Nikolov, M. Thompson, T. Stefanov, A. D. Pimentel, S. Polstra, R. Bose, C. Zissulescu, and E. F. Deprettere. Daedalus: Toward Composable Multimedia MP-SoC Design. In Proceedings of the Design Automation Conference (DAC), pages 574-579, 2008.
V. Pareto. Cours d'Économie Politique, volume 1. F. Rouge &Cie., 1896.
F. Reimann, M. Glaß, C. Haubelt, M. Eberl, and J. Teich. Improving Platform-Based System Synthesis by Satisfiability Modulo Theories Solving. In Proceedings of the Conference on Hardware/Software Codesign and System Synthesis (CODES+ISSS), pages 135-144, 2010.
O. Roussel and V. Manquinho. Pseudo-Boolean and cardinality constraints. In Biere et al. [8], chapter 22, pages 695-733.
N. Satish, K. Ravindran, and K. Keutzer. A Decomposition-Based Constraint Optimization Approach for Statically Scheduling Task Graphs with Communication Delays to Multiprocessors. In Proceedings of the Design, Automation and Test in Europe (DATE), pages 57-62, 2007.
T. Schlichter, C. Haubelt, and J. Teich. Improving EA-based Design Space Exploration by Utilizing Symbolic Feasibility Tests. In Proceedings of Genetic and Evolutionary Computation Conference> (GECCO), pages 1945-1952, 2005.
H. M. Sheini and K. A. Sakallah. A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic. In Theory and Applications of Satisfiability Testing, pages 241-256, 2005.
J. Teich and C. Haubelt. Digitale Hardware/Software-Systeme - Synthese und Optimierung. Springer, Berlin, Heidelberg, 2007. 2. erweiterte Auflage.
L. Thiele, I. Bacivarov, W. Haid, and K. Huang. Mapping Applications to Tiled Multiprocessor Embedded Systems. In Proceedings of the International Conference on Application of Concurrency to System Design (ACSD), pages 29-40, 2007.
L. Thiele and E. Wandeler. Performance Analysis of Distributed Embedded Systems. In Embedded Systems Handbook, pages 15.1-15.18. CRC Press, Boca Raton, FL, 2006.
E. Zitzler, L. Thiele, M. Laumanns, C. Fonseca, and V. Grunert da Fonseca. Performance Assessment of Multiobjective Optimizers: An Analysis and Review. IEEE Transactions on Evolutionary Computation, 7(2):117-132, 2003.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode