Published: 19th September 2020
|Preface Francesco Ricca, Alessandra Russo, Sergio Greco, Nicola Leone, Alexander Artikis, Gerhard Friedrich, Paul Fodor, Angelika Kimmig, Francesca Lisi, Marco Maratea, Alessandra Mileo and Fabrizio Riguzzi
Invited talks (Main Conference)
|Applications of Answer Set Programming where Theory meets Practice Esra Erdem
|When Is It Morally Acceptable to Break the Rules? A Preference-Based Approach Francesca Rossi
|Formal Reasoning Methods for Explainability in Machine Learning Joao Marquez-Silva
|From Probabilistic Logics to Neuro-Symbolic Artificial Intelligence Luc De Readt
Invited talk (Women in Logic Prorgramming Track)
|Norms, Policy and Laws: Modelling, Compliance and Violation Marina De Vos
Panel in Machine Ethics (Invited Paper)
|Logic Programming and Machine Ethics Abeer Dyoub, Stefania Costantini and Francesca A. Lisi
|Datalog-Based Systems Can Use Incremental SMT Solving (Extended Abstract) Aaron Bembenek, Michael Ballantyne, Michael Greenberg and Nada Amin
|Splitting a Hybrid ASP Program Alex Brik
|Formal Semantics and Scalability for Datalog with Aggregates: A Cardinality-Based Solution (Extended Abstract) Carlo Zaniolo, Ariyam Das, Youfu Li, Mingda Li and Jin Wang
|Variant-based Equational Unification under Constructor Symbols Damián Aparicio-Sánchez, Santiago Escobar and Julia Sapiña
|Solving Gossip Problems using Answer Set Programming: An Epistemic Planning Approach Esra Erdem and Andreas Herzig
|Justifications for Goal-Directed Constraint Answer Set Programming Joaquín Arias, Manuel Carro, Zhuo Chen and Gopal Gupta
|SQuARE: Semantics-based Question Answering and Reasoning Engine Kinjal Basu, Sarat Chandra Varanasi, Farhad Shakerin and Gopal Gupta
|A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States (Extended Abstract) Loc Pham, Enrico Pontelli, Fabio Tardivo and Tran Cao Son
|A Hybrid Neuro-Symbolic Approach for Complex Event Processing (Extended Abstract) Marc Roig Vilamala, Harrison Taylor, Tianwei Xing, Luis Garcia, Mani Srivastava, Lance Kaplan, Alun Preece, Angelika Kimming and Federico Cerutti
|Data validation for Answer Set Programming (Extended Abstract) Mario Alviano and Carmine Dodaro
|Automated Aggregator - Rewriting with the Counting Aggregate Michael Dingess and Miroslaw Truszczynski
|Deriving Theorems in Implicational Linear Logic, Declaratively Paul Tarau and Valeria de Paiva
|A System for Explainable Answer Set Programming Pedro Cabalar, Jorge Fandinno and Brais Muñiz
|Tabling Optimization for Contextual Abduction Ridhwan Dewoprabowo and Ari Saptawijaya
|Burden of Persuasion in Argumentation Roberta Calegari and Giovanni Sartor
|Continuous Reasoning for Managing Next-Gen Distributed Applications Stefano Forti and Antonio Brogi
|Sequent-Type Calculi for Systems of Nonmonotonic Paraconsistent Logics Tobias Geibinger and Hans Tompits
|Enhancing Linear Algebraic Computation of Logic Programs Using Sparse Representation Tuan Nguyen Quoc, Katsumi Inoue and Chiaki Sakama
|LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories Wolf De Wulf and Bart Bogaerts
|Recursive Rules with Aggregation: A Simple Unified Semantics (Extended Abstract) Yanhong A. Liu and Scott D. Stoller
|Dynamic Multi-Agent Path Finding based on Conflict Resolution using Answer Set Programming Basem Atiq, Volkan Patoglu and Esra Erdem
|An application of Answer Set Programming in Distributed Architectures: ASP Microservices Stefania Costantini and Lorenzo De Lauretis
|Less Manual Work for Safety Engineers: Towards an Automated Safety Reasoning with Safety Patterns Yuri Gil Dantas, Antoaneta Kondeva and Vivek Nigam
Women in Logic Programming Track
|Modeling Bitcoin Lightning Network by Logic Programming (Extended Abstract) Damiano Azzolini, Elena Bellodi, Alessandro Brancaleoni, Fabrizio Riguzzi and Evelina Lamma
|A Machine Learning guided Rewriting Approach for ASP Logic Programs Elena Mastria, Jessica Zangari, Simona Perri and Francesco Calimeri
|Logical Judges Challenge Human Judges on the Strange Case of B.C.-Valjean Viviana Mascardi and Domenico Pellegrini
Sister Conferences and Journal Presentation Track
|Accountable Protocols in Abductive Logic Programming (Extended Abstract) Marco Gavanelli, Marco Alberti and Evelina Lamma
|Sampling-Based SAT/ASP Multi-Model Optimization as a Framework for Probabilistic Inference (Extended Abstract) Matthias Nickles
|Report: Datalog with Recursive Aggregation for Incremental Program Analyses (Extended Abstract) Tamás Szabó, Gabór Bergmann, Sebastian Erdweg and Markus Voelter
|Knowledge of Uncertain Worlds: Programming with Logical Constraints (Extended Abstract) Yanhong A. Liu and Scott D. Stoller
|A Simple Extension of Answer Set Programs to Embrace Neural Networks (Extended Abstract) Zhun Yang, Adam Ishay and Joohyung Lee
|Constraint Programming Algorithms for Route Planning Exploiting Geometrical Information Alessandro Bertagnon
|Research Summary on Implementing Functional Patterns by Synthesizing Inverse Functions Finn Teegen
|A Low-Level Index for Distributed Logic Programming Thomas Prokosch
|Extending Answer Set Programs with Neural Networks Zhun Yang
This volume contains the Technical Communications and the Doctoral Consortium papers of the 36th International Conference on Logic Programming (ICLP 2020), held virtually in Rende (CS), Italy, from September 20th to 25th, 2020. This is the first time that ICLP is run remotely together with all co-located events due to the COVID pandemic.
Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. The scope of the conference covers all areas of logic programming including, but not restricted to:
Besides the main track, ICLP 2020 included the following additional tracks and special sessions:
Applications Track: This track invites submissions of papers on emerging and deployed applications of LP, describing all aspects of the development, deployment, and evaluation of logic programming systems to solve real-world problems, including interesting case studies and benchmarks, and discussing lessons learned.
Sister Conferences and Journal Presentation Track: This track provides a forum to discuss important results related to logic programming that appeared recently (from January 2018 onwards) in selective journals and conferences but have not been previously presented at ICLP.
Research Challenges in Logic Programming Track: This track invites submissions of papers describing research challenges that an individual researcher or a research group is currently attacking. The goal of the track is to promote discussions, exchange of ideas, and possibly stimulate new collaborations. Papers submitted to this track do not go through the usual review and will not be published in the proceedings they will be distributed at the conference as a technical report.
Special Session. Women in Logic Programming: This track aims to increase the visibility and impact of women in LP. It invites submissions of papers in all areas of logic programming co-authored by at least one woman and includes invited talks and presentations by women in logic programming.
The organizers of ICLP 2020 were:General Chairs
Three kinds of submissions were accepted:
ICLP implemented the hybrid publication model used in all recent editions of the conference, with journal papers and Technical Communications (TCs), following a decision made in 2010 by the Association for Logic Programming. Papers of the highest quality were selected to be published as rapid publications in this special issue of TPLP. The TCs comprise papers which the Program Committee (PC) judged of good quality but not yet of the standard required to be accepted and published in TPLP as well as extended abstracts from the different tracks and dissertation project descriptions stemming from the Doctoral Program (DP) held with ICLP.
We have received 88 submissions of abstracts, of which 77 resulted in paper submissions, distributed as follows: ICLP main track (53), Applications track (7 full papers and 1 short papers), Sister Conferences and Journal Presentation track (6), Women in Logic Programming session (5 full papers and 3 short papers) and Research Challenge Track (2 short papers). The Program Chairs organized the refereeing process, which was undertaken by the PC with the support of external reviewers. Each technical paper was reviewed by at least three referees who provided detailed written evaluations. This yielded submissions short-listed as candidates for rapid communication. The authors of these papers revised their submissions in light of the reviewers suggestions, and all these papers were subject to a second round of reviewing. Of these candidates papers, 27 were accepted as rapid communications, to appear in the special issue. In addition, the PC recommended 40 papers to be accepted as technical communications, to appear at Electronic Proceedings in Theoretical Computer Science (EPTCS) either as full papers or extended abstracts, of which 38 were also presented at the conference (2 were withdrawn).
We are deeply indebted to the Program Committee members and external reviewers, as the conference would not have been possible without their dedicated, enthusiastic and outstanding work. The Program Committee members of ICLP 2020 were:
|Manuel V. Hermenegildo
|Guillermo R. Simari
|Tran Cao Son
|Francesca Alessandra Lisi
|Yanhong A. Liu
The Program Committee members of the Applications track were:
The external reviewers were:
|Jose F. Morales
|Sarat Chandra Varanasi
The 16th Doctoral Consortium (DC) on Logic Programming was held in conjunction with ICLP 2020. It attracts Ph.D. students in the area of Logic Programming Languages from different backgrounds (e.g. theoretical, implementation, application) and encourages a constructive and fruitful advising. Topics included: theoretical foundations of logic and constraint logic programming, sequential and parallel implementation technologies, static and dynamic analysis, abstract interpretation, compilation technology, verification, logic-based paradigms (e.g., answer set programming, concurrent logic programming, inductive logic programming) and innovative applications of logic programming. This year the Doctoral Consortium accepted 4 papers in the areas described above. We warmly thank all student authors, supervisors, referees, co-chairs, members of the program committee and the organizing team that made the Doctoral Consortium greatly successful.
The DC Program Committee members were:
|Jose F. Moralesr
|Zeynep G. Saribatur
We would also like to express our gratitude to the full ICLP 2020 organization committee. Our gratitude must be extended to Torsten Schaub as current President and Thomas Eiter as incoming President of the Association of Logic Programming (ALP), to Marco Gavanelli in the role of conference-coordinator for ALP, to all the members of the ALP Executive Committee and to Mirek Truszczynski, Editor-in-Chief of TPLP. Also, to the staff at Cambridge University Press for their assistance. We would also like to thank Rob van Glabbeek, Editor-in-Chief of EPTCS, for helping the Program Chairs with their prompt support. Finally, we wish to thank each author of every submitted paper, since their efforts keep the conference alive and the participants to ICLP for bringing and sharing their ideas and latest developments. This is particularly appreciated in this 36th edition of the conference which has run during the unprecedented time of the COVID pandemic.
|Francesco Ricca, Alessandra Russo, Sergio Greco, Nicola Leone, Alexander Artikis, Angelika Kimmig,
|Gerhard Friedrich, Fabrizio Riguzzi, Paul Fodor, Marco Maratea, Francesca Alessandra Lisi, Alessandra Mileo (Eds.)
We have been investigating applications of Answer Set Programming (ASP) in various domains, ranging from historical linguistics and bioinformatics to economics and robotics. In these applications, theory meets practice around challenging computational problems, and they all start a journey towards benefiting science and life. ASP plays an important role in this journey, sometimes as a declarative programming paradigm to solve hard combinatorial search problems (e.g., phylogeny reconstruction for Indo-European languages, multi-agent path finding in autonomous warehouses, matching problems in economics), and sometimes as a knowledge representation paradigm to allow deep reasoning and inferences over incomplete heterogeneous knowledge and beliefs of agents (e.g., hybrid planning for robotic manipulation, diagnostic reasoning in cognitive factories, explanation generation for biomedical queries). In this talk, we will share our experiences from such different applications of ASP, and discuss its role and usefulness from different perspectives.
Humans make moral judgements about their own actions and the actions of others. Sometimes they make these judgements by following a utilitarian approach, other times they follow simple deontological rules, and yet at other times they find (or simulate) an agreement among the relevant parties. To build machines that behave similarly to humans, or that can work effectively with humans, we must understand how humans make moral judgements. This includes when to use a specific moral approach and how to appropriately switch among the various approaches. We investigate how, why, and when humans decide to break some rules. We study a suite of hypothetical scenarios that describes a person who might break a well established norm and/or rule, and asked human participants to provide a moral judgement of this action.
In order to effectively embed moral reasoning capabilities into a machine we model the human moral judgments made in these experiments via a generalization of CP-nets, a common preference formalism in computer science. We describe what is needed to both model the scenarios and the moral decisions, which requires an extension of existing computational models. We discuss how this leads to future research directions in the areas of preference reasoning, planning, and value alignment.
The forecasted success of machine learning (ML) hinges on systems that are robust in their operation and that can be trusted. This talk overviews recent efforts on applying automated reasoning tools in explaining non-interpretable (black-box) ML models, for assessing heuristic explanations, but also for learning interpretable ML models. Concretely, the talk overviews existing approaches for producing rigorous explanations of black-box models, and assesses the quality of widely used heuristic approaches for computing explanations. In addition, the talk discusses properties of rigorous explanations. Finally, the talk briefly overviews ongoing work on learning interpretable ML models.
A central challenge to contemporary AI is to integrate learning and reasoning. The integration of learning and reasoning has been studied for decades already in the fields of statistical relational artificial intelligence and probabilistic programming. StarAI has focussed on unifying logic and probability, the two key frameworks for reasoning, and has extended this probabilistic logics machine learning principles. I will argue that StarAI and Probabilistic Logics form an ideal basis for developing neuro-symbolic artificial intelligence techniques. Thus neuro-symbolic computation = StarAI + Neural Networks. Many parallels will be drawn between these two fields and will be illustrated using the Deep Probabilistic Logic Programming language DeepProbLog.
Norms, policy and laws all focus on describing desired behaviour of actors, whether they are humans, agents or processes. The actual behaviour of the actor can then be checked against this and compliance or violation potentially respectively rewarded or penalised. This talk explores the use of answer set programming in modelling the modelling, verification and compliance of these norms, policy and laws, both at the modelling stage but also in a running system. We demonstrate how this technology can be used to detect inconsistencies between sets of norms/policies/norms and how they could possibly be resolved
Satisfiability modulo theories (SMT) solving is a powerful tool. However, any client of an SMT solver faces the challenge of using the solver efficiently. In particular, modern SMT solvers support incremental solving, so there is often an advantage to asking queries in an order that lets the solver reuse work from earlier queries when answering new ones. Thus, clients are incentivized to pose queries in a way that has good "solver locality" and is amenable to effective incremental solving.
Because they are both used for automated reasoning tasks, there is a natural appeal to augmenting logic programming systems with the capabilities of SMT solving. One such hybrid system, Formulog , does this by extending Datalog with terms that represent SMT formulas and an interface to an external SMT solver. However, the notion of "solver locality" raises a potential problem for Formulog and other logic programming systems that embrace Kowalski's principle  of separating the logic of a computation from its control: The programmer cannot easily control the order of computations, and the language runtime might perform them in an order that has low solver locality.
For example, consider using Formulog to explore simple paths in a directed graph whose edges are labeled with SMT propositions. A path is explored only if the conjunction of its edge labels is satisfiable. This computation would have clearly good solver locality if it consecutively checked the satisfiability of similar paths (e.g., paths with a large common prefix); such a result might be achieved by using a sequential depth-first search (DFS) of the graph, starting at each node in turn. However, the same is not obviously the case for Formulog: because of its parallelized bottom-up evaluation algorithm, it effectively performs a breadth-first search of the graph starting from each node of the graph in parallel. Thus, paths discovered around the same time might not share a very large common prefix; in fact, they might be completely disjoint! Given the lack of obvious solver locality, it is not clear if this Formulog program should expect any advantage from incremental SMT solving.
We show empirically that, even in this setting, incremental SMT solving can in fact speed up logic programs that make SMT queries. We do so by evaluating the effectiveness of two lightweight encoding mechanisms that mediate between Formulog and an external SMT solver. The mechanisms use different capabilities defined in the SMT-LIB standard : the first explicitly manages a solver's assertion stack, while the second checks satisfiability under retractable assumptions. The latter strategy consistently leads to speedups over a non-incremental baseline across a variety of benchmarks involving different SMT solvers and SMT-LIB logics, suggesting that logic programming systems can indeed take advantage of incremental, black-box SMT solving.
A Formulog user builds complex terms representing SMT formulas and reasons
about them with built-in operators like
When an SMT operator is invoked, the Formulog runtime takes the SMT query,
serializes it into the SMT-LIB format, ships it off to an external solver, and
returns the result.
The serialization code takes a list of conjuncts as input; its
job is to assert these conjuncts to the SMT solver in a way that
leads to efficient solving.
We evaluate three different strategies for SMT clients: a baseline non-incremental
strategy and two incremental strategies.
First, some background: SMT-LIB-compatible solvers maintain a stack of
Frames can be pushed on and popped off the stack using the commands
When a frame is popped, the solver's state is reset to the state it had before
that frame was added, forgetting any assertions made since the corresponding
push command along with any consequences derived from those assertions.
Our baseline, non-incremental strategy clears the solver's assertion state between every satisfiability check: When it serializes an SMT query, it generates code that pushes a fresh frame on the stack, asserts each conjunct, checks for satisfiability, and then pops the frame it added.
Our second strategy (PP) explicitly
pops the solver's stack to enable
When serializing a query, PP
pops off frames
until the solver's assertion stack is a prefix of the current list of
pushes assertions for each of the remaining conjuncts of the query, and then checks for satisfiability.
PP provides incremental solving when adjacent queries share large
PP works well for clients who explore a constraint space
(since the stack disciplines match up), but
penalizes clients who use search techniques that align less well with using a
stack (breadth-first search, heuristic searches, etc.).
Our final strategy (CSA) uses the
check-sat-assuming SMT-LIB command, which checks
the satisfiability of the solver's assertion state assuming particular
truth values for some given boolean variables.
CSA uses a layer of indirection to treat the solver's assertion
state as a cache of assertions that can be enabled or
disabled for a particular query :
instead of asserting a
conjunct $\phi$ directly, CSA asserts the
implication $x \implies \phi$, where $x$ is a fresh boolean variable.
To check the satisfiability of a query including $\phi$,
we include $x$ in the list of literals provided to the
Formulog's CSA client maintains a map from conjuncts to
boolean variables to keep track of which variables should be enabled for a
particular query and to ensure that no conjunct is ever asserted
more than once.
SMT clients using CSA need not manage an explicit stack of assertions; there is no penalty for exploring the constraint space in a way that does not align well with using a stack. Intuitively, CSA should be a boon for logic programming systems like Formulog that do not use a DFS-based search.
We empirically evaluated two hypotheses: (H1) Formulog should be able to take advantage of incremental SMT solving; i.e., either PP or CSA should outperform the non-incremental baseline strategy on most benchmarks; (H2) CSA should deliver more consistent and more substantial speedups than PP. To evaluate these hypotheses, we tested the relative performance of the three strategies on three Formulog programs given a variety of inputs.
The first program performs symbolic execution  over a simple imperative language. We ran the tool on six different input programs. We tried the solvers Z3 (v4.8.8) , CVC4 (v1.7) , and Boolector (v3.2.1)  (all set to use the logic QF_ABV). In all 18 cases, the baseline was bested by an incremental strategy (H1); CSA achieved the best speedup in 12 of these cases (H2).
The second program type checks programs written in Dminor , a language with refinement types that are encoded as SMT formulas. We ran the type checker on three input programs, using the solver Z3 with the logic ALL. CSA had the best improvement over the baseline in all three cases (H1, H2).
The third program computes reachability on graphs with edges labeled by propositions; a path is feasible only if the conjunction of the propositions along that path is satisfiable. We computed reachability on 24 random graphs in various bit vector and linear integer arithmetic (LIA) logics. We used the solvers Z3, CVC4, and Yices (v2.6.2) , and additionally Boolector for the graphs with bit vector formulas. The incremental strategies were better than the baseline on 60 of 84 experiments (H1), and CSA had the best improvement in 59 cases (H2). Of the cases where there was no gain by using incremental solving, 14 were clustered in the experiments with logics combining LIA and arrays.
Overall, out of 105 experiments, either PP or CSA beat the non-incremental baseline in 81 cases (H1✓). CSA provided a speedup in 79 cases, compared to 39 for PP; there were only two cases where PP provided a speedup and CSA did not, and only five where both strategies led to speedups but PP was faster than CSA (H2✓). Thus, our evaluation confirms our hypotheses: CSA is an effective, lightweight mechanism for integrating a logic programming system with an incremental SMT solver.
A growing body of recent research is showing that the use of aggregates in recursive Datalog programs allows a concise declarative formulation for algorithms that support with superior performance and scalability a wide range of Big Data applications, including graph and ML applications [2, 3, 4, 5, 6,7]. Yet the full deployment of this potentially disruptive logic programming technology requires a formal semantics which is simple enough to be used with confidence by everyday programmers in writing their applications. To address this need, we propose a cardinality-based approach that; identify the class of programs that use the count aggregate in recursion; and combine (i) Stable-Model (SM)semantics with (ii) very efficient; operational semantics that is also conducive to scalability via parallelization.
On objective (i) we seek to provide criteria and techniques which allow users to; prove that their programs have a Stable Model semantics,without having to rely on the formal definition of this semantics. However, for certain programs, their SM semantics is not conducive to an efficient and scalable implementation. We provide a simple criterion to identify programs along; with some hints on how to re-express such applications by program that is free of this problem. However, for a majority of programs of practical interest, an efficient and scalable computation of their SM semantics is at hand immediately using the notions of pre-mappability of extrema  and stale-synchronous parallelism. In fact the programs described in the above references fall in this second category that combine formal semantics with efficient and scalable implementation.
Moreover, as we deal with the other aggregates, we realize that they can all be defined by adding to the basic definition of count simple monotonic extensions needed to express the specific aggregate. In all cases, the value of the aggregate is returned when all the members of the set have been counted, i.e., when the computation of count reaches its max value.Thus the SM and fixpoint properties of programs containing arbitrary aggregates and their combinations remain those we have derived for count. Indeed, this approach has allowed us to express with formal SM and superior performance and scalability a wide range of algorithms used in graph, ML and KDD applications [1, 2, 4, 5, 6, 7]. Furthermore, query languages, such as SQL, can greatly benefit from these advances [2,7].