Preface

This volume contains the Technical Communications and the Doctoral Consortium papers of the 35th International Conference on Logic Programming (ICLP 2019), held in Las Cruces, New Mexico, USA, from September 20th to 25th, 2019.

Since the first conference held in Marseille in 1982, ICLP has been the premier international event for presenting research in logic programming. Contributions are sought in all areas of logic programming, including but not restricted to:

Foundations:

Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation.

Languages:

Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Modules, Meta-programming, Logic-based domain-specific languages, Programming Techniques.

Declarative programming:

Declarative program development, Analysis, Type and mode inference, Partial evaluation, Abstract interpretation, Transformation, Validation, Verification, Debugging, Profiling, Testing, Execution visualization

Implementation:

Virtual machines, Compilation, Memory management, Parallel/distributed execution, Constraint handling rules, Tabling, Foreign interfaces, User interfaces.

Related Paradigms and Synergies:

Inductive and Co-inductive Logic Programming, Constraint Logic Programming, Answer Set Programming, Interaction with SAT, SMT and CSP solvers, Logic programming techniques for type inference and theorem proving, Argumentation, Probabilistic Logic Programming, Relations to object-oriented and Functional programming.

Applications:

Databases, Big Data, Data integration and federation, Software engineering, Natural language processing, Web and Semantic Web, Agents, Artificial intelligence, Computational life sciences, Education, Cybersecurity, and Robotics.

Besides the main track, ICLP 2019 included the following additional tracks and special sessions:

Applications Track: This track invited submissions of papers on emerging and deployed applications of logic programming, 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 provided a forum to discuss important results related to logic programming that appeared recently (from January 2017 onwards) in selective journals and conferences, but have not been previously presented at ICLP.

Research Challenges in Logic Programming Track: This track invited 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.

Special Session. Women in Logic Programming: This special session included an invited talk and presentations describing research by women in logic programming.

The organizers of ICLP 2019 were:

• Enrico Pontelli, New Mexico State University
• Tran Cao Son, New Mexico State University

• Esra Erdem, Sabanci University
• Germán Vidal, Universitat Politecnica de Valencia

• Ferdinando Fioretto, Georgia Institute of Technology

• Martin Gebser, University of Klagenfurt and Graz University of Technology

• Pedro Cabalar, University of Corunna

• Paul Fodor, Stony Brook New York
• Daniela Inclezan, Miami University

• José Morales, IMDEA Software Institute
• Orkunt Sabuncu, TED University

• Andrea Formisano, Universita' di Perugia
• Fangkai Yang, NVIDIA Corporation

• Bart Bogaerts, Vrije Universiteit Brussel
• Giovambattista Ianni, Universita' della Calabria

• Alessandro dal Palu, Universita' di Parma
• Amelia Harrison, University of Texas at Austin and Google Inc.
• Joohyung Lee, Arizona State University

• Alicia Villanueva, Universitat Politecnica de Valencia
• Marina De Vos, University of Bath

Three kinds of submissions were accepted:

• Technical papers for technically sound, innovative ideas that can advance the state of logic programming;
• Application papers that impact interesting application domains;
• System and tool papers which emphasize novelty, practicality, usability, and availability of the systems and tools described.

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 a 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 122 submissions of abstracts, of which 92 resulted in full submissions, distributed as follows: ICLP main track (59), Applications track (9 full papers and 9 short papers), Sister Conferences and Journal Presentation track (11), and Women in Logic Programming session (4). 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 enabled a list of papers to be 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, 30 were accepted as rapid communications, to appear in the special issue of TPLP. In addition, the PC recommended 45 papers to be accepted as technical communications, either as full papers or extended abstracts, of which 44 were also presented at the conference (1 was 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 2019 were:

The Program Committee members of the Applications track were:

The Program Committee members of the Special Session: Women in Logic Programming were:

The external reviewers were:

The 15th Doctoral Consortium (DC) on Logic Programming was held in conjunction with ICLP 2019. 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 12 papers (out of 15 submissions) 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:

We would also like to express our gratitude to the full ICLP 2019 organization committee. Our gratitude must be extended to Torsten Schaub, who is serving in the role of President of the Association of Logic Programming (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.

Bart Bogaerts, Esra Erdem, Paul Fodor, Andrea Formisano, Giovambattista Ianni, Daniela Inclezan,

Germán Vidal, Alicia Villanueva, Marina De Vos, Fangkai Yang  (Eds.)

What Logic Can Do for AI Today

I will discuss a number of roles for logic in AI today, which include probabilistic reasoning, machine learning and explaining AI systems. For probabilistic reasoning, I will show how probabilistic graphical models can be compiled into tractable Boolean circuits, allowing probabilistic reasoning to be conducted efficiently using weighted model counting. For machine learning, I will show how one can learn from a combination of data and knowledge expressed in logical form, where symbolic manipulations end up playing the key role. Finally, I will show how some common machine learning classifiers over discrete features can be compiled intro tractable Boolean circuits that have the same input-output behavior, allowing one to symbolically explain the decisions made by these numeric classifiers.

ASP Applications for AI and Industry

Answer Set Programming (ASP) evolved from Logic Programming, Deductive Databases, Knowledge Representation, and Nonmonotonic Reasoning, and serves as a flexible language for solving problems in a declarative way: the user does not need to provide an algorithm for solving the problem; rather, (s)he specifies the properties of the desired solutions by means of formal representations in a logic program. The ASP system automatically computes the solutions having the desired properties. ASP implements McCarty's view of the computation of intelligent artifacts, and it is considered a major paradigm of logic-based Artificial Intelligence (AI). After more than twenty years from the introduction of ASP, the core solving technology has become mature, and a number of practical applications are available.

In this talk, we illustrate our experience to bring AI and ASP from research to industry, through the development of advanced applications with DLV—one of the major ASP systems. DLV has undergone an industrial exploitation by DLVSYSTEM, a spin-off company of University of Calabria, and has been successfully used in several real-world applications. In particular, in the talk, we first present our framework for AI application development, which is based on the latest evolutions of DLV in a server-like platform. Then, we focus on the description of some industry-level applications of ASP, including success stories and ongoing developments. Eventually, we share the lessons that we have learned in our experience, and discuss our outlook over the possible roles of ASP-based technologies in the modern AI spring.

Reward Machines: Structuring Reward Function Specifications and Reducing Sample Complexity in Reinforcement Learning

Humans have evolved languages over thousands of years to provide useful abstractions for understanding and interacting with each other and with the physical world. Such languages include natural languages, mathematical languages and calculi, and most recently formal languages that enable us to interact with machines via human-interpretable abstractions. In this talk, I present the notion of a Reward Machine, an automata-based structure that provides a normal form representation for reward functions. Reward Machines can be used natively to specify complex, non-Markovian reward-worthy behavior. Furthermore, a variety of compelling human-friendly (formal) languages can be used as reward specification languages and straightforwardly translated into Reward Machines, including variants of Linear Temporal Logic (LTL), LDL, and a variety of regular languages. Reward Machines can also be learned and can be used as memory for interaction in partially-observable environments. By exposing reward function structure, Reward Machines enable reward-function-tailored reinforcement learning, including tailored reward shaping and Q-learning. Experiments show that such reward-function-tailored algorithms significantly outperform state-of-the-art (deep) RL algorithms, solving problems that otherwise can't reasonably be solved and critically reducing the sample complexity.

System PROJECTOR: An Automatic Program Rewriting Tool for Non-Ground Answer Set Programs

Answer set programming is a popular constraint programming paradigm that has seen wide use across various industry applications. However, logic programs under answer set semantics often require careful design and nontrivial expertise from a programmer to obtain satisfactory solving times. In order to reduce this burden on a software engineer we propose an automated rewriting technique for non-ground logic programs that we implement in a system PROJECTOR. We conduct rigorous experimental analysis, which shows that applying system PROJECTOR to a logic program can improve its performance, even after significant human-performed optimizations. This talk will present PROJECTOR and considered experimental analysis in great detail.

Knowledge Representation and Reasoning Issues in Natural Language Question Answering

In this tutorial we will discuss various Natural Language Question Answering challenges that have been proposed, including some that focus on the need for common sense reasoning, and how knowledge representation and reasoning may play an important role in addressing them. We will discuss various aspects such as: what knowledge representation formalisms have been used, how they have been used, where to get the relevant knowledge, how to search for the relevant knowledge, how to know what knowledge is missing and how to combine reasoning with machine learning. We will also discuss extraction of relevant knowledge from text, learning relevant knowledge from the question answering datasets and using crowdsourcing for knowledge acquisition. We will discuss KR challenges that one faces when knowledge is extracted or learned automatically versus when they are manually coded. Finally we will discuss using natural language as a knowledge representation formalism together with natural language inference systems and semantic textual similarity systems.

Constraint Programming for Resource Management

Resource allocation poses unique challenges ranging from load balancing in heterogeneous environments to privacy concerns and various service-level agreements. In this tutorial, we highlight industrial applications from distinct problem domains that span both extremes of the optimization landscape; operational decision making in real-time and resource provisioning for future considerations. Motivated by real-world business requirements, we will walk through how Constraint Programming delivers effective solutions in both settings and compare & contrast it with alternative approaches such as heuristics and mathematical programming.

While solving large-scale problems is of great practical importance, there is a need for solutions that are not only efficient but also flexible, easy to update, and maintain. We show how Constraint Programming neatly suits the needs of such dynamic environments with continually changing requirements.

Tractable Probabilistic Circuits

Probabilistic models like Bayesian Networks enjoy a considerable amount of attention due to their expressiveness. However, they are generally intractable for performing exact probabilistic inference. In contrast, tractable probabilistic circuits guarantee that exact inference is efficient for a large set of queries. Moreover, they are surprisingly competitive when learning from data.

In this tutorial, I present an excursus over the rich literature on tractable circuit representations, disentangling and making sense of the "alphabet soup" of models (ACs, CNs, DNNFs, d-DNNFs, OBDDs, PSDDs, SDDs, SPNs, etc) that populate this landscape. I explain the connection between logical circuits and their probabilistic counterparts used in machine learning, as well as the connection to classical tractable probabilistic models such as tree-shaped graphical models. Under a unifying framework, I discuss which structural properties delineate model classes and enable different kinds of tractability. While doing so, I highlight the sources of intractability in probabilistic inference and learning, review the solutions that different tractable representations adopt to overcome them, and discuss what they are trading off to guarantee tractability. I will touch upon the main algorithmic paradigms to automatically learn both the structure and parameters of these models from data.

Finally, I argue for high-level representations of uncertainty, such as probabilistic programs, probabilistic databases, and statistical relational models. These pose unique challenges for probabilistic inference and learning that can only be overcome by high-level reasoning about their first-order structure to exploit symmetry and exchangeability, which can also be done within the probabilistic circuit framework.

Towards Computing Abstract Distances in Logic Programs

Many practical static analyzers are based on the theory of Abstract Interpretation. The basic idea behind this technique is to interpret (i.e., execute) the program over a special abstract domain \(D_\alpha\) to obtain some abstract semantics \(S_\alpha\) of the program \(P\), which will over-approximate every possible execution of \(P\) in the standard (concrete) domain \(D\). This makes it possible to reason safely (but perhaps imprecisely) about the properties that hold for all such executions.

When designing or choosing an abstract interpretation-based analysis, a crucial issue is the trade-off between cost and accuracy, and thus research in new abstract domains, widenings, fixpoints, etc., often requires studying this trade-off. However, while measuring analysis cost is typically relatively straightforward, having effective accuracy metrics is much more involved. There have been a few proposals for this purpose, including, e.g., probabilistic abstract interpretation and some metrics in numeric domains, but they have limitations and in practice most studies come up with ad-hoc accuracy metrics, such as counting the number of program points where one analysis is strictly more precise than another.

We propose a new approach for measuring the accuracy of abstract interpretation-based analyses in (C)LP. It is based on defining distances in abstract domains, denoted abstract distances, and extending them to distances between inferred semantics or whole analyses of a given program, over those domains. The difference in accuracy between two analyses can then be measured as the distance between them, and the accuracy of an analysis can be measured as the distance to the actual abstract semantics, if known.

We first develop some general theory on metrics in abstract domains. Two key points to consider here are the structure of an abstract domain as a lattice and the relation between the concrete and abstract domains. With regard to the first point, we survey and extend existing theory and proposals for distances in a lattice \(L\). The distances are often based in a partial distance \(d_\sqsubseteq : \{(a,b) ~|~ (a,b) \in L \times L, ~ a \sqsubseteq b ~\} \rightarrow \mathbb{R}\) between related elements of the lattice, or in a monotonic size \(size : L \rightarrow \mathbb{R}\). With regard to the second, we study the relation between distances \(d\) and \(d_\alpha\) in the concrete and abstract domains, and the abstraction and concretization functions \(\alpha : D \rightarrow D_\alpha\), \(\gamma : D_\alpha \rightarrow D\). In that sense we observe that both \(\alpha\) and \(\gamma\) induce distances \(d_\alpha^\gamma : D_\alpha \times D_\alpha \rightarrow \mathbb{R}, ~ d_\alpha^\gamma(a,b) = d(\gamma(a),\gamma(b))\) and \(d^\alpha : D \times D \rightarrow \mathbb{R}, ~ d^\alpha(A,B)=d_\alpha(\alpha(A),\alpha(B))\) in the abstract and concrete domains from distances \(d\) and \(d_\alpha\) in the concrete and abstract domains respectively.

We then build on this theory and ideas in order to propose metrics for a number of common domains used in (C)LP analysis. In particular we define formally distances for the domains share and regular types, and show that they are indeed metrics. The domain share abstracts information about variable sharing between terms in a substitutions, and the distance there builds on a notion of size in the domain, based on the set-based structure of the domain. The regular types domain abstracts information about the shape of the terms in a substitution, and the distance there is based on the abstraction of a Hausdorff distance between sets of terms in the concrete domain.

We then extend these metrics to distances between abstract interpretation-based analyses of a whole program, that is, distances in the space of AND-OR trees that represent the abstract execution of a program over an abstract domain. We proposed three extensions in increasing order of complexity. The first is the top distance, which only considers the roots of the AND-OR trees, i.e., the top result or abstract answer of the analysis, and computes the abstract distance between the abstract substitutions in those roots. The second is the flat distance, which groups together all nodes of the tree corresponding to the same program point, by means of the least upper bound operation, and is based on the abstract distances between the resulting abstract substitutions in each program point. The third is the tree distance, which considers the whole tree, computing the abstract distances node to node, and therefore it is a metric. All these distances between analyses are thus parametric on an abstract distance in the underlying abstract domain.

These distances can then be used to compare quantitatively the accuracy of different abstract interpretation-based analyses of a whole program, by just calculating the distances between the representation of those analyses as AND-OR trees. This results in a principled methodology to measure differences of accuracy between analyses, which can be used to measure the accuracy of new fixpoints, widenings, etc. within a given abstract interpretation framework, not requiring knowledge of its implementation (i.e., apart from the underlying domain, everything else can be treated as a black box, if the framework provides a unified representation of analysis results as AND-OR trees).

Finally, we implement the proposed distances within the CiaoPP framework (Hermenegildo et al. 2005) and apply them to study the accuracy-cost trade-off of different sharing-related (C)LP analyses over a number of benchmarks and a real program. The domains share-free, share, def, and share-free clique, with a number of widenings, are used for this experiment. For the accuracy comparison, all the analyses results are translated so as to be expressed in terms of a common domain, share (i.e., their accuracy is compared only with respect of the sharing information they infer), and the loss of accuracy for each one is computed as the distance to a most precise analysis computed as the ''intersection'' between all of them. The results align with our a-priori knowledge, confirming the appropriateness of the approach, but also allow us to obtain further useful information and insights on where to use each domain. These preliminary results lead us to believe that this application of distances is promising in a number of contexts such as debugging the accuracy of analyses or calibrating heuristics for combining different domains in portfolio approaches.

References

1. This document is an extended abstract of Technical Report CLIP-2/2019.0 (Casso et al. 2019). Research partially funded by MINECO project TIN2015-67522-C3-1-R TRACES and Comunidad de Madrid project S2018/TCS-4339 BLOQUES-CM, co-funded by EIE Funds of the European Union.

Reasoning about Problems of Actual Causation Using an Action Language Approach

The goal of this abstract is to discuss an investigation into the suitability of action languages for representing and reasoning about actual causation. Also referred to as causation in fact, actual cause is a broad term that encompasses all possible antecedents that have played a meaningful role in producing a consequence. Reasoning about actual cause concerns determining how a particular consequence came to be in a given scenario, and the topic been studied extensively in numerous fields including philosophy, law, and, more recently, computer science and artificial intelligence.

Attempts to mathematically characterize actual causation have largely pursued counterfactual analysis of structural equations (e.g. [1,2]), neuron diagrams (e.g. [3]), and other logical formalisms (e.g., [4]). Counterfactual accounts of actual causation are inspired by the human intuition that if $X$ caused $Y$, then not $Y$ if not $X$ [5]. At a high level, this approach involves looking for possible worlds in which $Y$ is true and $X$ is not. If such a world is found, then $X$ is not a cause of $Y$. It has been widely documented, however, that the counterfactual criteria alone is problematic and fails to recognize causation in a number of common cases such as overdetermination (i.e., multiple causes for the effect), preemption (i.e., one cause ``blocks'' another's effect), and contributory causation (i.e., causes must occur together to achieve the effect) (see e.g. [6]). Subsequent approaches have addressed some of the shortcomings associated with the counterfactual criterion by modifying the existing definitions, introducing supplemental definitions, and by modeling time with some improved results. However, in spite of decades of research into this topic, there is currently no agreed-upon counterfactual definition of actual cause.

We believe that the controversy surrounding this issue is due, at least in part, to the fact that the counterfactual approach to reasoning about what could have happened does not necessarily reflect the nature of the problem at hand. Rather, the problem of determining how an outcome of interest was actually caused in a given scenario ostensibly requires reasoning about the causal dynamics of the scenario itself to identify one or more events that contributed to the outcome's causation.

Another contributing factor may be the representation of the scenarios themselves. For instance, a surprising number of approaches have formalized scenarios without representing time or even ordering of events. More recent approaches have identified this as problematic and have attempted to represent the events of a scenario as sequences of events. While sequences of events indeed represent a step in the right direction, we believe that representing scenarios as the evolution of state in response to events is closer to how we mentally represent scenarios. As we discuss in this abstract, representing scenarios in this way provides us with much of the information that we need to reason about how an outcome of interest has come to be.

To these ends, we have developed a novel framework that departs from the counterfactual intuition and enables reasoning about the underlying causal mechanisms of scenarios in order to reason about and explain actual causation. Our framework uses techniques from Reasoning about Actions and Change (RAC) to support reasoning about domains that change over time in response to a sequence of events. The action language $\mathcal{A}\mathcal{L}$ [7] enables us to encode knowledge of the direct and indirect effects of events in a given domain in a straightforward way, as well as to represent scenarios as the evolution of state over the course of the scenario's events.

$\mathcal{A}\mathcal{L}$ is centered around a discrete-state-based representation of the evolution of a domain in response to events. The language builds upon an alphabet consisting of a set $\mathcal{F}$ of fluents and a set $\mathcal{E}$ of elementary events. Fluents are boolean properties of the domain, whose truth value may change over time. A (fluent) literal is a fluent $f$ or its negation $\neg f$. An elementary event is denoted by its element $e$ of $\mathcal{E}$, and a compound event} $\epsilon$ is a set of elementary events. A state $\sigma$ is a set of literals and if a fluent $f\in\sigma$, we say that $f$ holds in $\sigma$. An action description is a set of $\mathcal{AL}$ laws which encode knowledge of the direct effects of elementary events (dynamic laws) on the state of the world, the ramifications of elementary events (state constraints), and the conditions under which elementary events cannot occur (executability conditions). Only events can change the value of a fluent, either as a direct effect or as a ramification of its occurrence. Finally, the semantics of $\mathcal{AL}$ are given by a transition diagram -- a directed graph $\langle N, A \rangle$ such that $N$ is the collection of all states of $AD$ and $A$ is the set of all triples $\langle \sigma, \epsilon, \sigma'\rangle$ where $\sigma$, $\sigma'$ are states and $\epsilon$ is a compound event that occurs in $\sigma$ and results in state $\sigma'$ as per the laws of the action description $AD$. A sequence $\langle \sigma_1, \epsilon_1, \sigma_2, \ldots, \epsilon_{k}, \sigma_{k+1} \rangle$ is a path of $\tau(AD)$ if every triple $\langle\sigma_i,\epsilon_i,\sigma_{i+1}\rangle$, $1\leq i \leq k$, in the path is a valid transition.

In our framework, the elements of $\mathcal{AL}$'s semantics are used to define notions of direct and indirect causation, and the language's solution to the frame problem can be leveraged to detect the "appearance" of an outcome of interest in a scenario. Consider the well-known Yale Shooting Problem from [8]:

Shooting a turkey with a loaded gun will kill it. Suzy loads the gun and then shoots the turkey. What is the cause of the turkey's death?

Given the events of the scenario and the knowledge of the effects of events, we can intuitively conclude that Suzy shooting the turkey with a loaded gun is the cause of death. We can construct an action description describing the causal knowledge as a set $AD$ containing two dynamic laws. The first law states that the event of loading a gun causes the gun to be loaded, and the second states that shooting at a turkey causes it to die if the gun is loaded. The scenario itself can be represented as a path $\langle \sigma_1,\epsilon_1,\sigma_2,\epsilon_2,\sigma_3\rangle$. The turkey is alive and the gun is not loaded in state $\sigma_1$, Suzy loads the gun in $\epsilon_1$ which causes the gun to be loaded in $\sigma_2$, and she then shoots the turkey in $\epsilon_2$ which results in its death in $\sigma_3$. Using our framework, we first identify $\sigma_3$ as the transition state of turkey's death by noticing the turkey was alive in $\sigma_2$ but is no longer living in $\sigma_2$. We then identify $\epsilon_2$ as the causing compound event of the turkey's death because the turkey's status changed after the compound event's occurrence. Finally, we look at the event of shooting the turkey in $\epsilon_2$ together with the law describing the effect of shooting the turkey to determine that this elementary event is the direct cause of the fluent literal representing the turkey's death.

The framework also enables reasoning about the indirect causation of fluents by way of an event's ramifications. Specifically, we define indirect causation of fluent literals in terms of static chains which describe a unique chain of state changes originating from an event's direct effects that results in a fluent holding by way of the state constraints in the action description. In previous work, we defined indirect cause by characterizing whether or not an event would cause an outcome of interest if it were to occur on its own [9]. However, this approach produces counter-intuitive results in cases that are specific to transition diagrams. The new approach described here resolves the shortcomings of the original definition. We have tested the framework on several additional examples from the literature, including variants of the Yale Shooting Problem [10], Pearl's well-known Firing Squad example [1] and the track switching scenario [11]. In the interest of space, we will not present the examples in this abstract, however, our investigation has shown that the framework does not share the shortcomings of counterfactual approaches (e.g., overdetermination, preemption, and joint causation) in a number of traditionally challenging cases.

The aim of the work discussed here is to lay the foundations of actual causal explanation from the standpoints described above. An important next step will be to conduct a comparative analysis with related approaches to reasoning about actual causation on these and other examples. Additional open problems involve investigating extensions of the framework and input language to support the representation of non-determinism, time-dependent effects, probabilities, and triggered events by exploring relationships with additional languages whose semantics can be given by a transition diagram. It is also worth noting that our choice of $\mathcal{AL}$ as the underlying formalism has useful practical implications. As demonstrated by a substantial body of literature (see, e.g., [12]), $\mathcal{AL}$ lends itself naturally to an automated translation to Answer Set Programming [13-14], using which, reasoning tasks of considerable complexity can be specified and executed. We strongly believe that extending and implementing the framework in these ways can be beneficial to domains that rely on monitoring continuous streams of events whose effects may require explanation (e.g. self-driving cars, Internet of Things and digital twin applications, and cyber-physical security systems).

References

1. Pearl, J. 2000. Causality: models, reasoning and inference. Econometric Theory 19, 675-685, 46
2. Halpern, J. Y. and Pearl, J. 2005. Causes and explanations: A structural-model approach. part i: Causes. The British journal for the philosophy of science 56, 4, 843-887
3. Hall, N. 2007. Structural equations and causation. Philosophical Studies 132, 1, 109-136
4. Beckers, S. and Vennekens, J. 2016. A general framework for defining and extending actual causation using cp-logic. International Journal of Approximate Reasoning 77, 105-126
5. Lewis, D. 1973. Causation. The journal of philosophy 70, 17, 556-567
6. Glymour, C. and Danks, D. 2010. Actual causation: a stone soup essay. Synthese 175, 2, 169-192.
7. Baral, C. and Gelfond, M. 2000. Reasoning agents in dynamic domains. In Logic-based artificial intelligence. Springer, 257-379
8. Hall, N. 2004. Two concepts of causation. Causation and counterfactuals, 225-276
9. LeBlanc, E., Balduccini, M., and Vennekens, J. 2019. Explaining actual causation via reasoning about actions and change. In European Conference on Logics in Artificial Intelligence. Springer, 231-246
10. Hanks, S. and McDermott, D. 1987. Nonmonotonic logic and temporal projection. Artificial intelligence 33, 3, 379-412
11. Hall, N. 2000. Causation and the price of transitivity. The Journal of Philosophy 97, 4, 198-222.
12. Balduccini, M. and Michael G. Diagnostic reasoning with a-prolog. Theory and Practice of Logic Programming. 3.4+ 5 (2003): 425-461.
13. Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming. ICLP/SLP. Vol. 88. 1070-1080
14. Gelfond, M. and Lifschitz, V. 1991. Classical negation in logic programs and disjunctive databases. New generation computing 9, 3-4, 365-385

On Improving Unit Testing in IDEs for ASP (Extended Abstract)

Unit testing frameworks are nowadays considered a best practice, foregone in almost all modern software development processes, to achieve rapid development of correct specifications. The first unit testing specification language for Answer Set Programming (ASP) was proposed in 2011 ([1]) as a feature of the ASPIDE ([2]) development environment. Later, a more portable unit testing language was included in the LANA annotation language ([3]). In this paper we propose a new unit test specification language that allows one to inline tests within ASP program and a complexity-aware test execution mechanism. Test-case specifications are transparent to the traditional evaluation, but can be interpreted by a specific testing tool. Thus, we present a novel environment supporting test driven development (TDD) ([4]) of ASP programs.

An usage example of the test annotations language can be found in Figure 1, which contains an instance of the graph coloring problem (3-colorability). This instance produces six answer sets according to the assignments of the colors to the specified nodes. In order to test whether the rules behave as expected, we have to be able to reference the rules under test. As we do not want to test facts, we assign the names r1 and r2 to the rules in Lines 6 and 8. Additionally we assign these rules to a block, which has been defined in Line 4. Afterwards we are able to reference the rules under test inside the @test(...) annotation starting in Line 10. First we specify the name of the test case and the rules under test, which is the block rulesToTest in this case. While referencing the block is more convenient, we could also reference the rules directly by writing scope = { "r1", "r2" }. Input rules can be defined with the property input, which are joined with the rules under test during test execution. They are equivalent to the facts of the program in this case, but can be different for more complex test specifications. With the property assert we can now define assertions that have to be fulfilled in order to execute the test with positive result. For this simple instance of the graph coloring problem, we can test whether the atom col(1, red) is true in at least two answer sets (Line 15).

 
 1 %** Test graph **%
 2 node(1). node(2). node(3). edge(1, 2). edge(1, 3). edge(2, 3).
 3
 4 %** @block(name="rulesToTest") **%
 5 %** @rule(name="r1", block="rulesToTest") **%
 6 col(X, red) | col(X, blue) | col(X, green) :- node(X).
 7 %** @rule(name="r2", block="rulesToTest") **%
 8 :- edge(X, Y), col(X,C), col(Y,C).
 9
10 %**  @test(name = "checkRules",
11        scope = { "rulesToTest" },
12        input = "node(1). node(2). node(3). edge(1, 2). edge(1, 3). 
13            edge(2, 3).",
14        assert = {
15            @trueInAtLeast(number = 2, atoms = "col(1, red).")
16        }
17    )   **%

Figure 1: Example of usage of the test annotation language with a program written in ASP-Core-2 syntax.

Test case execution is performed on an answer set solver. However, before execution the specified input rules (property input of the annotation @test(...)) are joined with the rules under test to form an intermediate program. Afterwards this intermediate program is enriched with test-case specific ASP rules and executed on the solver. Depending on the assertions of the test case, the intermediate program is enriched with auxiliary atoms and/or constraints to guarantee a complexity-aware execution. For the example in Figure 1 the intermediate program will contain an additional constraint, as seen in the following translation:

node(1). node(2). node(3). edge(1, 2). edge(1, 3). edge(2, 3).
col(X, red) | col(X, blue) | col(X, green) :- node(X).
:- edge(X, Y), col(X,C), col(Y,C).
:- not col(1, red).

By adding the integrity constraint :- not col(1, red). the program aims to find an answer set that fulfills the assertion. The execution will determine if there are at least 2 models, while the solver is configured to search for 2 answer sets. Based on that, the test fails, resp. passes if there are 2 answer sets. For this example the test will pass, as there are exactly 2 answer sets containing col(1, red). Both the annotation-based test specification language, as well as the execution mechanism are implemented as part of a web-based development environment called ASP-WIDE. It can be installed as a standalone application in any computer with a modern (java-script enabled) web browser and Java 8 installed. ASP-WIDE can be downloaded from: http://www.mat.unical.it/ricca/asptesting/asp-wide_1.0-beta4.zip, and the sources of the environment are distributed under GPL licence.

References

1. Onofrio Febbraro, Nicola Leone, Kristian Reale & Francesco Ricca (2011): Unit Testing in ASPIDE. In: INAP/WLP, Springer, Berlin, Heidelberg, pp. 345-364, doi:10.1007/978-3-642-41524-1_21.

2. Onofrio Febbraro, Kristian Reale & Francesco Ricca (2011): ASPIDE: Integrated Development Environment for Answer Set Programming. In: LPNMR, Springer, Berlin, Heidelberg, pp. 317-330, doi:10.1007/978-3-642-20895-9_37.

3. Marina De Vos, Doga Gizem Kisa, Johannes Oetsch, Jörg Pührer & Hans Tompits (2012): Annotating answer-set programs in LANA. In: TPLP, pp. 619-637, doi:10.1017/S147106841200021X.

4. Steven Fraser, Kent L. Beck, Bill Caputo, Tim Mackinnon, James Newkirk & Charlie Poole (2003): Test Driven Development (TDD). XP Springer, Berlin, Heidelberg, pp. 459-462, doi:10.1007/3-540-44870-5_84.

Towards a General Framework for Static Cost Analysis of Parallel Logic Programs

Estimating in advance the resource usage of computations is useful for a number of applications. Examples include granularity control in parallel/distributed systems, automatic program optimization, verification of resource-related specifications, and detection of performance bugs, as well as helping developers make resource-related design decisions. Besides time and energy, we assume a broad concept of resources as numerical properties of the execution of a program, including the number of execution steps, the number of calls to a procedure, the number of network accesses, the number of transactions in a database, and other user-definable resources. The goal of automatic static analysis is to estimate such properties (prior to running the program with concrete data) as a function of input data sizes and possibly other (environmental) parameters.

Due to the heat generation barrier in traditional sequential architectures, parallel computing, with (possibly heterogeneous) multi-core processors in particular, has become the dominant paradigm in current computer architectures. Predicting resource usage on such platforms poses important challenges. Most work on static resource analysis has focused on sequential programs, and comparatively less progress has been made on the analysis of parallel programs, or on parallel logic programs in particular. The significant body of work on static analysis of sequential logic programs has already been applied to the analysis of other programming paradigms, including imperative programs. This is achieved via a transformation into Horn clauses.

In this paper we concentrate on the analysis of parallel Horn clause programs, which could be the result of such a translation from a parallel imperative program or be themselves the source program. Our starting point is the standard general framework of CiaoPP for setting up parametric relations representing the resource usage (and size relations) of programs. This is based on the well-developed technique of setting up recurrence relations representing resource usage functions parameterized by input data sizes, which are then solved to obtain (exact or safely approximated) closed forms of such functions (i.e., functions that provide upper or lower bounds on resource usage). The framework is doubly parametric: first, the costs inferred are functions of input data sizes, and second, the framework itself is parametric with respect to the type of approximation made (upper or lower bounds), and to the resource analyzed. We build on this and propose a novel, general, and flexible framework for setting up cost equations/relations which can be instantiated for performing static resource usage analyses of parallel logic programs for a wide range of resources, platforms, and execution models. Such analyses estimate both lower and upper bounds on the resource usage of a parallel program as functions on input data sizes. We have instantiated the framework for dealing with Independent And-Parallelism (IAP), which refers to the parallel execution of conjuncts in a goal. However, the results can be applied to other languages and types of parallelism, by performing suitable transformations into Horn clauses.

Independent And-Parallelism arises between two goals (or other parts of executions) when their corresponding executions do not affect each other. For pure goals (i.e., without side effects) a sufficient condition for the correctness of IAP is the absence of variable sharing at run time among such goals. (Restricted) IAP has traditionally been expressed using the &/2 meta-predicate as the constructor to represent the parallel execution of goals. In this way, the conjunction of goals (i.e., literals) p & q in the body of a clause will trigger the execution of goals p and q in parallel, finishing when both executions finish.

Automatically finding closed-form upper and lower bounds for recurrence relations is an uncomputable problem. For some special classes of recurrences, exact solutions are known, for example for linear recurrences with one variable. For some other classes, it is possible to apply transformations to fit a class of recurrences with known solutions, even if this transformation obtains an appropriate approximation rather than an equivalent expression. Particularly for the case of analyzing independent and-parallel logic programs, nonlinear recurrences involving the \(max\) operator are quite common. For example, if we are analyzing elapsed time of a parallel logic program, a proper parallel aggregation operator is the maximum between the times elapsed for each literal running in parallel. To the best of our knowledge, no general solution exists for recurrences of this particular type. However, in this paper we identify some common cases of this type of recurrences, for which we obtain closed forms that are proven to be correct.

We have implemented a prototype of our approach, extending the existing resource usage analysis framework of CiaoPP. The implementation basically consists of the parameterization of the operators used for sequential and parallel cost aggregation, i.e., for the aggregation of the costs corresponding to the arguments of ,/2 and &/2, respectively. This allows the user to define resources in a general way, taking into account the underlying execution model. We introduce a new general parameter that indicates the execution model the analysis has to consider. For our current prototype, we have defined two different execution models: standard sequential execution, represented by seq, and an abstract parallel execution model, represented by par(n), where \(n \in \mathbb{N} \cup \{\infty\}\). The abstract execution model par\((\infty)\) is similar to the work and depth model presented and used extensively in previous work. Basically, this model is based on considering an unbounded number of available processors to infer bounds on the depth of the computation tree. The work measure is the amount of work to be performed considering a sequential execution. These two measures together give an idea on the impact of the parallelization of a particular program. The abstract execution model par(n), where \(n \in \mathbb{N}\), assumes a finite number \(n\) of processors.

For the evaluation of our approach, we have analyzed a set of benchmarks that exhibit different common parallel patterns, together with the definition of a set of resources that help understand the overall behavior of the parallelization. The results show that most of the benchmarks have different asymptotic behavior in the sequential and parallel execution models. As mentioned before, this is an upper bound for an ideal case, assuming an unbounded number of processors. Nevertheless, such upper-bound information is useful for understanding how the cost behavior evolves in architectures with different levels of parallelism. In addition, this dual cost measure can be combined together with a bound on the number of processors in order to obtain a general asymptotic upper bound.

References

1. This document is an extended abstract of Technical Report CLIP-1/2019.0 (Klemen et al. 2019). Research partially funded by MINECO project TIN2015-67522-C3-1-R TRACES and Comunidad de Madrid project S2018/TCS-4339 BLOQUES-CM, co-funded by EIE Funds of the European Union.

Pre-Mappable Constraints in Recursive Programs

The concept of Pre-Mappable (PreM) constraints in recursive queries has made possible (i) the declarative expression of classical algorithms in Datalog and other logic-based languages, and (ii) their efficient execution in implementations that achieve superior performance and scalability on multiple platforms. In this extended abstract, we present a concise analysis of this very general property and characterize its different manifestations for different constraints and rules.

Keywords: Aggregates in Recursive Programs, Constraint Optimization, Non-Monotonic Semantics

1. Introduction

The growth of BigData applications adds new vigor to the vision of Datalog researchers who sought to combine the expressive power demonstrated by recursive Prolog programs with the performance and scalability of relational DBMSs. Their research led to the delivery of a first commercial Datalog system [1] and also had a significant impact on other languages and systems. In particular, DBMS vendors introduced support for recursive queries into their systems and into the SQL-2003 standards by adopting Datalog's (a) stratified semantics for negation and aggregates, (b) optimization techniques that include (i) seminaive fixpoint computation, (ii) constant pushing for left/right-linear rules, and (iii) magic sets for linear rules. However, many algorithms and queries of practical interest cannot be expressed efficiently, or cannot be expressed at all, using stratified programs. This has motivated much research work seeking to go beyond stratification, often through the introduction of more powerful semantics, including semantics based on locally stratified programs, well-founded models and stable models.

On the other hand, concise expression and efficient support for a wide range of polynomial time algorithms, while keeping a stratification-based formal semantics, was made possible by the recent introduction of pre-mappable constraints [8]. Indeed, besides providing a very general optimization criterion for pushing constraints of various types into recursion, PreM delivers major semantic benefits for extrema constraints. In fact, when PreM holds for min or max in recursive rules, then such min or max can be transferred out of the recursive definition and used as post-constraints in a final rule, yielding an equivalent stratified program that defines the declarative semantics of the original program. Thus, PreM sits at the confluence of the two lines of research investigating (a) non-monotonic semantics for aggregates, and (b) optimization by pushing constraints. The ability of using PreM extrema in recursive programs also extends to the count and sum aggregates [7], entailing the ability of expressing a wide variety of algorithms which, using a version of seminaive fixpoint optimized for aggregates [6], execute with superior performance and scalability. For instance, complex graph queries can be expressed more concisely and executed more efficiently in SQL with PreM aggregates in recursion than in the special-purpose graph languages and systems as has been demonstrated in the recently proposed work [6], which addresses this area of weakness of the SQL-2003 compliant DBMSs.

In order to realize the significant potential offered by PreM, the concept must be well-understood and its validity must be easy to verify for the applications of interest. Therefore in this extended abstract, we present a concise analysis of the property and discover that different types of PreM occur for different constraints and rules, and we discuss the PreM types and proving techniques defined for specifically for min and max constraints.

2. Pre-Mappable Constraints in Graph Queries

In the example below, the predicate ${\tt path(X,Y,D)}$ is defined by the non-recursive rule $r_{1.1}$, which will be called an exit rule, and the recursive rule $r_{1.2}$. $r_{1.3}$ is the final post-condition rule that finds the minimal distance of each node from node ${\tt a}$ by applying the constraint ${\tt is\_min((X,Y),D)}$, where ${\tt (X, Y)}$ is the group-by argument and ${\tt D}$ is the cost argument. (The group-by argument contains zero or more variables, whereas the cost argument contains exactly one variable.)

$ r_{1.1}: {\tt path(X, Y, D)} \leftarrow {\tt arc(X, Y, D)}.$
$ r_{1.2}: {\tt path(X, Y, D)} \leftarrow {\tt path(X, Z, Dxz)}, {\tt arc(Z, Y, Dzy)}, {\tt D=Dxz+Dzy}. $
$ r_{1.3}: {\tt shortestpath(X, Y, D)} \leftarrow {\tt path(X, Y, D)}, {\tt X=a}, {\tt is\_min((X,Y), D)}. $

The formal semantics of extrema constraints can be easily reduced to that of negation. For instance, in the above example, the semantics of ${\tt is\_min((X,Y),D)}$ can be defined by re-writing $r_{1.3}$ into $r_{1.4}$ and $r_{1.5}$, where $r_{1.4}$ uses negation to express the constraint that a triplet ${\tt (X,Y,D)}$ is acceptable only if there is no other triplet having the same ${\tt (X,Y)}$ and a smaller ${\tt D}$. While this ensures the program has a perfect-model semantics, the iterated fixpoint computation of such a model is extremely inefficient and may not even terminate in presence of cycles.

$ r_{1.4}: {\tt shortestpath(X, Y, D)} \leftarrow {\tt path(X, Y, D)}, {\tt \neg betterpath(X, Y, D)}. $
$ r_{1.5}: {\tt betterpath(X, Y, D)} \leftarrow {\tt path(X, Y, D)}, {\tt path(X, Y, Dxy)}, {\tt Dxy < D}. $

Following the results in [8], PreM addresses this inefficiency by pushing the ${\tt is\_min}$ constraint inside recursion, as shown in rules $r_{2.1}$ and $r_{2.2}$. This transformation is equivalence-preserving [2] and more efficient since the program below reaches the minimal fixpoint in finite number of steps. Whenever this equivalence-preserving transformation holds, we say the given constraint $\gamma$ is Pre-Mappable (PreM) onto the program $P$. Formally, $\gamma$ is PreM when for every interpretation $I$ of $P$, we have $\gamma(T(I)) = \gamma(T(\gamma(I)))$, where $T$ denotes the Immediate Consequence Operator for the recursive rules of $P$ [8].

$ r_{2.1}: {\tt path(X, Y, D)} \leftarrow {\tt arc(X, Y, D)}.$
$ r_{2.2}: {\tt path(X, Y, D)} \leftarrow {\tt path(X, Z, Dxz)}, {\tt arc(Z, Y, Dzy)}, {\tt D=Dxz+Dzy}, {\tt is\_min((X,Y), D)}. $
$ r_{2.3}: {\tt shortestpath(X, Y, D)} \leftarrow {\tt path(X, Y, D)}, {\tt X=a}. $

[6] demonstrated that one can easily verify if PreM holds during the execution of a program by simply comparing $\gamma(T(I))$ and $\gamma(T(\gamma(I)))$ at each step of the recursive evaluation. However, strictly speaking, more formal tools [9] are required to prove that PreM holds for any possible execution of a given program. For example in the above program, PreM is trivially satisfied by base rules such as $r_{2.1}$ [8], and therefore one only needs to verify if PreM holds for the recursive rule $r_{2.2}$. One can easily examine this by proving that an additional constraint $\bar{\gamma} = {\tt is\_min((X,Z),Dxz)}$ can be imposed on $I ={\tt path(X, Z, Dxz)}$ without changing the result obtained from using only the constraint $\gamma = {\tt is\_min((X,Y),Dxz+Dzy)}$. Indeed every ${\tt (X,Z,Dxz)}$ that violates $\bar{\gamma}$ produces an ${\tt (X,Y,D)}$ atom that also violates $\gamma$ and it is thus eliminated.

We next introduce two special cases of PreM along with their formal definitions. As evident in our following examples, these narrow definitions of specific instances of PreM are much easier to observe and verify.

• Intrinsic PreM (or iPreM): The PreM of a constraint $\gamma$ upon $T(I)$ will be called intrinsic when $T(I) = T(\gamma(I))$. To understand this, assume we replace $\tt D=Dxz+Dzy$ with, say, $\tt D = 3.14 * Dzy$ in rule $r_{2.2}$. Then obviously, the value of $\tt Dxz$ does not, in any way, affect the result computed in the head of the rule $r_{2.2}$. Thus, we could even select the min of these $\tt Dxz$ values, thereby eventually having $T(I)= T(\gamma(I))$ i.e. $\gamma$ is iPreM in this case.
• Radical PreM (or rPreM): The PreM of a constraint $\gamma$ upon $T(I)$ will be called radical when $\gamma(T(I)) = T(\gamma(I))$. Consider the constraint $\tt X=a$ in rule $r_{2.3}$ that specifies that we are only interested in the shortest paths that originate from node $\tt a$. This constraint can be pushed all the way to the non-recursive base rule $r_{2.1}$, leaving the recursive rule unchanged, yielding the exact same results. This exemplifies rPreM, which has been extensively researched in the Datalog literature, since it provides a very efficient optimization for equality constraints.

References

1. Molham Aref, Balder ten Cate, Todd J. Green, Benny Kimelfeld, Dan Olteanu, Emir Pasalic, Todd L. Veldhuizen & Geoffrey Washburn (2015): Design and Implementation of the LogicBlox System. In: SIGMOD'15.
2. Tyson Condie, Ariyam Das, Matteo Interlandi, Alexander Shkapsky, Mohan Yang & Carlo Zaniolo (2018): Scaling-up reasoning and advanced analytics on BigData. TPLP 18(5-6), pp. 806-845.
3. Ariyam Das, Sahil M. Gandhi & Carlo Zaniolo (2018): ASTRO: A Datalog System for Advanced Stream Reasoning. In: CIKM'18, pp. 1863-1866.
4. Ariyam Das, Youfu Li, Jin Wang, Mingda Li & Carlo Zaniolo (2019): BigData Applications from Graph Analytics to Machine Learning by Aggregates in Recursion. In: ICLP'19.
5. Ariyam Das & Carlo Zaniolo (2019): A Case for Stale Synchronous Distributed Model for Declarative Recursive Computation. In: ICLP'19.
6. Jiaqi Gu, Yugo Watanabe, William Mazza, Alexander Shkapsky, Mohan Yang, Ling Ding & Carlo Zaniolo (2019): RaSQL: Greater Power and Performance for Big Data Analytics with Recursive-aggregate-SQL on Spark. In: SIGMOD'19.
7. Mirjana Mazuran, Edoardo Serra & Carlo Zaniolo (2013): Extending the Power of Datalog Recursion. The VLDB Journal 22(4), pp. 471-493.
8. Carlo Zaniolo, Mohan Yang, Matteo Interlandi, Ariyam Das, Alexander Shkapsky & Tyson Condie (2017): Fixpoint semantics and optimization of recursive Datalog programs with aggregates. TPLP 17(5-6), pp. 1048-1065.
9. Carlo Zaniolo, Mohan Yang, Matteo Interlandi, Ariyam Das, Alexander Shkapsky & Tyson Condie (2018): Declarative BigData Algorithms via Aggregates and Relational Database Dependencies. In: AMW'18.

Tree Decomposition Rewritings for Optimizing Logic Programs under Answer Set Semantics

Answer Set Programming (ASP) [3, 9] is a declarative programming paradigm proposed in the area of non-monotonic reasoning and logic programming, nowadays supported by a number of efficient implementations [6, 8]. Computational problems are encoded by logic programs whose intended models, called answer sets, correspond one-to-one to solutions. Typically, the same computational problem can be encoded by means of many different ASP programs which are semantically equivalent; however, real ASP systems may perform very differently when evaluating each one of them. On the one hand, this is due to specific aspects of the ASP system at hand as, for instance, adopted algorithms and optimizations; on the other hand, specific structural properties of the program can make computation easier or harder. Thus, some expert knowledge can be required in order to select the best encoding when performance is crucial. This, in a certain sense, conflicts with the declarative nature of ASP that, ideally, should free the users from the burden of the computational aspects. For this reason, ASP systems tend to be endowed with proper pre-processing means aiming at making performance less encoding-dependent; intuitively, this also eases and fosters the usage of ASP in practice. The idea of transforming logic programs has been explored in past literature, to different extents, such as verification, performance improvements, etc. (see, just for instance [12] and more recent related works).

In this abstract we focus on ASP, and briefly survey a heuristic-guided strategy for automatically optimizing ASP encodings originally proposed in [5] and then extended in [7]. The strategy relies on proper adaptation of hypergraph tree decompositions techniques for rewriting logic rules, and makes use of custom heuristics in order to foresee if and to what extent the application of rewritings is convenient; an implementation has been integrated into the DLV [1] system, and in particular into the grounding subsystem I-DLV [4]. For all details and more formal material we refer to [5, 7].

Tree Decompositions for Rewriting ASP Rules. ASP program can be rewritten by making use of tree decompositions and hypergraphs. Hypergraphs can be used for describing the structure of many computational problems, and, in general, decompositions can be used to divide these structures into different parts. In this way, the solution(s) of a given problem can be obtained by a polynomial divide-and-conquer algorithm that properly exploits this division [10]. Based on such ideas, one can represent an ASP rule as an hypergraph [11], decompose it and then build, starting from the resulting tree decomposition, a set of new rules that are equivalent to the original one, yet typically shorter. For instance, the lpopt [2] tool uses tree decompositions for rewriting a program before it is fed to an ASP system. Interestingly, more than one decomposition is possible for each rule, in general.

A Heuristic-guided Decomposition Algorithm. As already noted, different yet equivalent programs require, in general, significantly different evaluation times; hence, one can wonder whether it is convenient or not to rewrite a program by means of decomposition techniques, and which decomposition is preferable among the many possible. The work in [7] introduces a smart decomposition algorithm for reasonably and effectively addressing the discussed issues. Roughly, the algorithm receives a rule as input, and outputs either a set of rules constituting the preferred decomposition, or the original rule; to this end, it relies on proper heuristics for: (i) estimating the cost of the evaluation if the rule stays in its original form; (ii) estimating the cost of the evaluation if the rule is substituted by a given decomposition; (iii) decide among two given decomposition which one is more likely to be convenient; (iv) estimate if decomposing is convenient. The definition of the heuristics strongly depend both on the ASP system at hand and on the main goals of the optimization, and this is why the algorithm is given in a general form and any actual implementation requires to precisely customize it by providing proper estimating criteria for handling points (i)-(iv) above. In [7] we reported on an implementation into the I-DLV system [4]. The adopted heuristics have been designed with the explicit aim to optimize the "grounding" (or instantiation) process, that is, one of the two relevant phases of the typical ASP computation, which transforms the program into an equivalent variable-free one. We tested the resulting implementation in order to assess the effectiveness of both the method and the implementation.

Experiments. Table 1 reports a summary of experiments conducted in [7]. It depicts the behaviour of the system with and without the integration of the algorithm. Two sets of data are reported: the first refers to the whole collection of problem domains, while the second to the subset of "affected domains", i.e., problems where significant differences on performance are reported, either positive or negative. The first two columns report performance of the two system configurations, respectively, while the third reports the percentage gain achieved by the system thanks to the algorithm. On the overall, the experiments evidence a positive impact of the technique on grounding performance: a hundred of additional grounded instances (+6%), more than 80% of timeouts avoided, and no more instances remain unsolved because of the excessive amount of required memory. The impact is even more evident if we consider that average times are computed only over the set of instances that are solved by both configurations; still, the performance gain turns out to be over 30%.

References

1. Weronika T. Adrian, Mario Alviano, Francesco Calimeri, Bernardo Cuteri, Carmine Dodaro, Wolfgang Faber, Davide Fuscà, Nicola Leone, Marco Manna, Simona Perri, Francesco Ricca, Pierfrancesco Veltri & Jessica Zangari (2018): The ASP System DLV: Advancements and Applications. KI 32(2-3), pp. 177-179, doi:10.1007/s13218-018-0533-0. Available at https://doi.org/10.1007/s13218-018-0533-0.
2. Manuel Bichler, Michael Morak & Stefan Woltran (2016): lpopt: A Rule Optimization Tool for Answer Set Programming. Logic-Based Program Synthesis and Transformation - 26th International Symposium, LOPSTR 2016, Edinburgh, UK, September 6-8, 2016, Revised Selected Papers, Lecture Notes in Computer Science 10184, Springer, pp. 114-130,doi:10.1007/978-3-319-63139-4 7. Available at https://doi.org/10.1007/978-3-319-63139-4_7.
3. Gerhard Brewka, Thomas Eiter & Miroslaw Truszczynski (2011): Answer set programming at a glance. Communications of the ACM 54(12), pp. 92-103, doi:10.1145/2043174.2043195. Available at http://doi.acm.org/10.1145/2043174.2043195.
4. Francesco Calimeri, Davide Fuscà, Simona Perri & Jessica Zangari (2017): I-DLV: The new intelligent grounder of DLV. Intelligenza Artificiale 11(1), pp. 5-20, doi:10.3233/IA-170104. Available at https://doi.org/10.3233/IA-170104.
5. Francesco Calimeri, Davide Fuscà, Simona Perri & Jessica Zangari (2018): Optimizing Answer Set Computation via Heuristic-Based Decomposition. In Practical Aspects of Declarative Languages - 20th International Symposium, PADL 2018, Los Angeles, CA,USA, January 8-9, 2018, Proceedings, Lecture Notes in Computer Science 10702, Springer, pp. 135-151, doi:10.1007/978-3-319-73305-0_9. Available at https://doi.org/10.1007/978-3-319-73305-0_9.
6. Francesco Calimeri, Martin Gebser, Marco Maratea & Francesco Ricca (2016): Design and re-sults of the Fifth Answer Set Programming Competition. Artificial Intelligence 231, pp. 151-181, doi:10.1016/j.artint.2015.09.008. Available at https://doi.org/10.1016/j.artint.2015.09.008.
7. Francesco Calimeri, Simona Perri & Jessica Zangari (2019): Optimizing Answer Set Computation via Heuristic-Based Decomposition. Theory and Practice of Logic Programming 19(4), pp. 603-628, doi:10.1017/S1471068419000036, available at https://doi.org/doi:10.1017/S1471068419000036.
8. Martin Gebser, Nicola Leone, Marco Maratea, Simona Perri, Francesco Ricca & Torsten Schaub: Evaluation Techniques and Systems for Answer Set Programming: a Survey. In: Proceedings of IJCAI 2018: Survey Track, https://ijcai.org, pp. 5450-5456, doi:10.24963/ijcai.2018/769, available at https://doi.org/10.24963/ijcai.2018/769.
9. Michael Gelfond & Vladimir Lifschitz (1991): Classical Negation in Logic Programs and DisjunctiveDatabases. New Generation Computing 9(3/4), pp. 365-386, doi:10.1007/BF03037169. Available at https://doi.org/10.1007/BF03037169.
10. Georg Gottlob, Martin Grohe, Nysret Musliu, Marko Samer & Francesco Scarcello (2005): Hypertree De-compositions: Structure, Algorithms, and Applications. In: Graph-Theoretic Concepts in Computer Science, 31st International Workshop, WG 2005, Metz, France, June 23-25, 2005, RevisedSelected Papers, LNCS 3787, Springer, pp. 1-15, doi:10.1007/11604686_1. Available at https://doi.org/10.1007/11604686_1.
11. Georg Gottlob, Nicola Leone & Francesco Scarcello (2001): Hypertree Decompositions: A Survey. In: Proceeedings of Mathematical Foundations of Computer Science 2001, 26th International Symposium, MFCS 2001 Marianske Lazne, Czech Republic, August 27-31, 2001, LNCS 2136, Springer, pp. 37-57, doi:10.1007/3-540-44683-4_5. Available at https://doi.org/10.1007/3-540-44683-4_5.
12. Nicola Leone, Simona Perri & Francesco Scarcello (2001): Improving ASP Instantiators by Join-Ordering Methods. In: Proceedings of LPNMR 2001, Vienna, Austria, September 17-19, 2001, LNCS 2173, Springer, pp. 280-294, doi:10.1007/3-540-45402-0_21. Available at https://doi.org/10.1007/3-540-45402-0_21.
13. Michael Morak & Stefan Woltran (2012): Preprocessing of Complex Non-Ground Rules in Answer Set Programming. In: Technical Communications of the 28th Interna-tional Conference on Logic Programming, ICLP 2012, September 4-8, 2012, Budapest, Hungary, LIPIcs 17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 247-258, doi:10.4230/LIPIcs.ICLP.2012.247. Available at https://doi.org/10.4230/LIPIcs.ICLP.2012.247.

SDRL: Interpretable and Data-efficient Deep Reinforcement Learning Leveraging Symbolic Planning

SDRL: Interpretable and Data-efficient Deep Reinforcement Learning Leveraging Symbolic Planning

Deep reinforcement learning (DRL) has gained great success by learning directly from high-dimensional sensory inputs ([1]), yet is criticized for the lack of data-efficiency and interpretability. Especially, interpretability of subtasks is critical in hierarchical decision-making since it enhances the transparency of black-box-style DRL methods and helps the RL practitioners to understand the high-level behavior of the system better ([2]).

To address the aforementioned issues, we propose the symbolic deep reinforcement learning (SDRL) framework in this work. Specifically, ASP-based logic programming is used for high-level symbolic planning, while DRL can be utilized to learn low-level control policy. In addition, there is an intermediate meta-learner that evaluates the learning performance and improves the goal of the planning. As a result, those three components cross-fertilize each other and eventually converge to an optimal symbolic plan along with the learned subtasks.

One of the contributions of this work is the novel paradigm that integrates symbolic planning with DRL, which can seamlessly take charge of subtask scheduling, data-driven subtask learning, and subtask evaluation. Meanwhile, experiments validate that interpretability can be achieved through explicitly encoding declarative knowledge and learning into human-readable subtasks, and also data-efficiency can be improved through automatic selecting and learning control policies of modular subtasks.

References

1. Mnih, V. and Kavukcuoglu, K. and Silver, D. and Rusu, A. A and Veness, J. and Bellemare, M. G. and Graves, A. and Riedmiller, M. and Fidjeland, A. K. and Ostrovski, G. and others (2015): Human-level control through deep reinforcement learning. Nature, 518(7540), 529. doi:10.1038/nature14236 .
2. Gilpin, L. H., Bau, D., Yuan, B. Z., Bajwa, A., Specter, M., & Kagal, L. (2018): Explaining explanations: An overview of interpretability of machine learning. In 2018 IEEE 5th International Conference on data science and advanced analytics (DSAA), pp. 80-89. doi:10.1109/DSAA.2018.00018.

Digital Forensics and Investigations Meet Artificial Intelligence

An investigation consists, in general terms, of the series of actions and initiatives implemented by the investigators (police and judges) in order to ascertain the "truth" and acquire all possible information and data about a perpetrated crime and related facts and logical implications. A large number of subjects are involved in this activity, where they cope with pursuing a criminal activity, which could be still in progress. In an accurate vision, and according to the Italian Code of Criminal Procedure, investigations can be defined as the set of activities carried out by the officers and agents of the criminal police. An investigation has the aim of establishing the existence of a crime and the consequences that it has determined (generic proof or "de delicto") and of identifying the criminals (specific proof or "de reo").

These activities start from the act of acquisition of the crime notice or the analysis of the crime scene itself. Through a series of initiatives and actions, the investigation allows the collection of data and elements which, according to certain deductive logical reasoning, should lead to draw conclusions. Investigative cases are usually complex and involve a number of factors that need to be taken into account. Most of collected data are nowadays obtained through digital devices and platforms either seized from the suspects, or available on the Internet or shared by telecommunication companies. Thus, Digital Forensics is a branch of criminalistics which deals with the identification, acquisition, preservation, analysis and presentation of the information content of computer systems, or in general of digital devices. In particular, the main focus of this paper is to address the phase of "Evidence Analysis", which copes with pieces of evidence derived and collected from various electronic devices involved in the crimes and related to their perpetrators. Such evidence is examined and aggregated so as to reconstruct possible events, event sequences and scenarios related to a crime. Results of the Evidence Analysis phase are then made available to law enforcement, investigators, intelligence agencies, public prosecutors, lawyers and judges.

Nowadays, commercial-off-the-shelf (COTS) software products exist to manage Digital Forensics cases. Such products are usually workflow-driven, and provide mechanisms for information access, for search and data visualization. However, support for the effective aggregation and organization of useful evidence is simply non-existent. Human experts proceed to the analysis of data, including temporal sequences, and reach their conclusions according to their intuition and their experience. A formal explanation of such conclusions cannot generally be provided. Often, different experts reach different conclusions, and the arguments that they provide in support seem equally valid.

Naturally, each case has distinct characteristics, and a variety of cases can be found. However, we may notice that cases can, after all, be considered as puzzles. Thanks to the experience gained by one of the authors over the years in investigations, we are able to claim with good reason that indeed a wide range of real cases can be mapped to computational problems, often to known ones. We recognize that each case has distinct characteristics, and a variety of cases can be found. So, in this paper we consider the mapping into computational logic formulations of a number of significant sample problems. We do not pretend though that every possible case is reducible to the problem templates that we consider here. Our wider long-term perspective is in fact to construct a tool-kit that can be extended in time, to provide support to the investigation activities, automating most of the low level data handling methods, and supporting the investigator at the abstract level as well. When applicable, computational logic formulations can generate all possible scenarios compatible with the case's data and constraints. In the general case, this can be of great help as the human expert might sometimes overlook some of the possibilities. This has been verified by everyday practice, where different experts often generate different interpretations.

With a future perspective, we may notice that logical methods, like for instance Answer Set Programming (ASP), could provide a broad range of proof-based reasoning functionalities (including, e.g., time and time intervals logic, causality, forms of induction, etc.) that can be possibly integrated into a declarative framework for Evidence Analysis where the problem specification and the computational program are closely aligned. The encoding of cases via such tools would have the benefit that (at least in principle) correctness of such declarative systems based on computational logic can be formally verified. Moreover, recent research has led to new methods for visualizing and explaining the results of computed answers (e.g., based on argumentation schemes). So, one could not only represent and solve relevant problems, but might also employ suitable tools to explain the conclusions (and their proofs) in a transparent, comprehensible and justified way.

The mapping of a case to a computational-logic-based formulation is clearly a responsibility of the analyst, who may hopefully succeed or possibly fail to devise it. In the future however, we envisage the specification and implementation of Decision Support Systems (DSS) to support the analysts in such task. Available investigative information should be treated, in this perspective, via algorithmic solutions whose correctness can be proven. A very important point concerns the complexity of the required algorithms. After a thorough analysis and systematization of past real cases, (with anonymised data), we have been able to assess that NP formulations are often sufficient, with few cases where one has to climb a further level of the polynomial hierarchy. The NP representation is mandatory, as in general the available data will not provide a unique solution, but rather a set of plausible scenarios which are compatible with what is known. In particular cases, the NP forensic formulation has a solution in P. Though an investigative case may involve several data, it translates in general into a relatively small or medium instance of an NP problem, solvable by state-of-the-art inference engines.

Towards Dynamic Answer Set Programming over Finite Traces

Answer Set Programming (ASP [8]) has become a popular approach to solving knowledge-intense combinatorial search problems due to its performant solving engines and expressive modeling language. However, both are mainly geared towards static domains and lack native support for handling dynamic applications. We have addressed this shortcoming over the last decade by creating a temporal extension of ASP [1] based on Linear Temporal Logic (LTL [9]) that has recently led to the temporal ASP systemtelingo[4]. The approach of LTL has however its limitations when it comes to expressing control over temporal trajectories. Such control can be better addressed with Dynamic Logic (DL[10]), offering a more fine-grained approach to temporal reasoning thanks to the possibility to form complex actions from primitive ones. To this end, DL relies on modal propositions, like [ $\rho$ ] $\phi$, to express that all executions of (complex) action $\rho$ terminate in a state satisfying $\phi$. As an example, consider a “Russian roulette” variation of the Yale-shooting-scenario, so the turkey is dead after we pull the trigger as many times as needed until we reach the loaded chamber. This can be expressed in DL via the proposition: \( [\mathbf{while}\;\neg \mathit{loaded}\;\mathbf{do}\;\mathit{trigger};\mathit{trigger}]\mathit{dead} \). The term within brackets delineates trajectories matching the regular expression \( (\neg\mathit{loaded}?;\mathit{trigger})^*;\mathit{loaded}?;\mathit{trigger} \), where $\phi?$ tests whether $\phi$ holds at the state at hand, and ‘;’ and ‘*’ are the sequential composition and iteration operators, respectively. With this, the above proposition is satisfied whenever the state following a matching trajectory entails dead.

This expressive power motivated us to introduce the basic foundations of an extension of ASP with dynamic operators from DL in [2,3]. In particular, we (i) introduce a general logical framework comprising previous dynamic and temporal extensions and (ii) elaborate upon a translation to propositional theories that can in turn be compiled into logic programs. To this end, we follow the good practice of first introducing an extension to ASP’s base logic, the Logic of Here-and-There(HT[6]), and then to devise an appropriate reduction. An HT interpretation (H,T) is a pair of interpretations that can be seen as being three-valued. Total interpretations satisfying a certain minimality condition are known to correspond to stable models; they are also referred to as equilibrium models, and the resulting logic is called Equilibrium Logic (EL). For capturing (linear) time, sequences of such HT interpretations are considered, similar to LTL. In accord with [5], we argue that such linear traces provide an appropriate semantic account of time in our context, and thus base also our dynamic extension of ASP on the same kind of semantic structures.

Our ultimate goal is to conceive an extension of ASP with language constructs from dynamic (and temporal) logic in order to provide an expressive computational framework for modeling dynamic applications. To address this in a semantically well founded way, we generalize in[3] the definition of Dynamic HT and EL (DHT/DEL[2]) to accommodate finite traces and augment it with a converse operator (in order to capture past temporal operators). This not only allows us to embed temporal extensions of ASP, such as Temporal Equilibrium Logic over finite traces (TEL$_f$[4]) along with its past and future operators, and more standard ones like LTL$_f$[5], but moreover provides us with blueprints for implementation on top of existing (temporal) ASP solvers like telingo. Indeed, DEL$_f$ can be regarded as a non-monotonic counterpart of LDL$_f$[5], being in an analogous relationship as classical and equilibrium logic, or SAT and ASP, respectively.

References

1. F. Aguado, P. Cabalar, M. Diéguez, G. Pérez & C. Vidal (2013): Temporal equilibrium logic: a survey. Journal of Applied Non-Classical Logics 23(1-2), pp. 2-24, doi:10.1080/11663081.2013.798985.
2. A. Bosser, P. Cabalar, M. Diéguez & T. Schaub (2018): Introducing Temporal Stable Models for Linear Dynamic Logic . In M. Thielscher, F. Toni & F. Wolter, editors: Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR’18), AAAI Press, pp. 12-21.
3. P. Cabalar, M. Diéguez & T. Schaub (2019): Towards Dynamic Answer Set Programming over finite traces. In M. Balduccini, Y. Lierler & S. Woltran, editors: Proceedings of the Fifteenth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR’19), Lecture Notes in Artificial Intelligence 11481, Springer-Verlag, pp. 148-162, doi:10.1007/978-3-030-20528-7_12.
4. P. Cabalar, R. Kaminski, T. Schaub & A. Schuhmann (2018): Temporal Answer Set Programming on Finite Traces. Theory and Practice of Logic Programming 18(3-4), pp. 406-420, doi:10.1017/S1471068418000297.
5. G. De Giacomo & M. Vardi (2013): Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In F. Rossi, editor: Proceedings of the Twenty-third International Joint Conference on Artificial Intelligence (IJCAI’13), IJCAI/AAAI Press, pp. 854-860.
6. A. Heyting (1930): Die formalen Regeln der intuitionistischen Logik. In: Sitzungsberichte der Preussischen Akademie der Wissenschaften, Deutsche Akademie der Wissenschaften zu Berlin, p. 42-56. Reprint in Logik-Texte: Kommentierte Auswahl zur Geschichte der Modernen Logik, Akademie-Verlag, 1986.
7. H. Levesque, R. Reiter, Y. Lespérance, F. Lin & R. Scherl (1997): GOLOG: A Logic Programming Language for Dynamic Domains. Journal of Logic Programming 31(1-3), pp. 59-83, doi:10.1016/S0743-1066(96)00121-5.
8. V. Lifschitz (1999): Answer set planning. In D. de Schreye, editor: Proceedings of the International Conference on Logic Programming (ICLP’99), MIT Press, pp. 23-37.
9. A. Pnueli (1977): The Temporal Logic of Programs. In: Proceedings of the Eight-teenth Symposium on Foundations of Computer Science (FOCS’77), IEEE Computer Society Press, pp. 46-57, doi:10.1109/SFCS.1977.32.
10. V. Pratt (1976): Semantical Consideration on Floyd-Hoare Logic. In: Proceedings of the Seventeenth Annual Symposium on Foundations of Computer Science (SFCS’76), IEEE Computer Society Press, pp. 109-121, doi:10.1109/SFCS.1976.27.

---

Hybrid Answer Set Programming for Design Space Exploration

Christian Haubelt (University of Rostock, Germany)
Kai Neubauer (University of Rostock, Germany)
Torsten Schaub (University of Potsdam, Germany)
Philipp Wanko (University of Potsdam, Germany)

1 Introduction

With increasing demands for functionality, performance, and energy consumption in both industrial and private environments, the development of corresponding embedded processing systems is becoming more and more intricate. Also, desired properties are conflicting and compromises have to be found from a vast number of options to decide the most viable design alternatives. Hence, effective Design Space Exploration (DSE; [4]) is imperative to create modern embedded systems with desirable properties; it aims at finding a representative set of optimal valid solutions to a design problem helping the designer to identify the best possible options.

In [2] and its follow-up paper [3], we developed a general framework based on Answer Set Programming (ASP) that finds valid solutions to the system design problem and simultaneously performs DSE to find the most favorable alternatives. In the past, meta-heuristic algorithms were used almost exclusively, but they do not guarantee optimality and are ineffective for finding feasible designs in highly constrained environments. ASP-based solutions alleviate this problem and have shown to be effective for system synthesis. Also, recent developments in ASP solving allow for a tight integration of background theories covering all (numeric) constraints occurring in DSE. This enables partial solution checking to quickly identify infeasible or suboptimal areas of the design space. Our work leverages these techniques to create a holistic framework for DSE using Hybrid Answer Set Programming.

2 Design Space Exploration

While DSE can be done at various abstraction levels, the overall goal is to identify optimal implementations given a set of applications and a hardware platform. Our work targets streaming applications (such as video decoders) and heterogeneous hardware platforms organized as networks on chip (such as many-core SoCs) described at the electronic system level. Here, applications are defined as task-level descriptions and hardware platforms comprise networks of processing and memory elements. The DSE problem is twofold: first, evaluate a single feasible implementation, called a design point, and second, cover multiple (optimal) design points of the design space during exploration.

Obtaining a feasible implementation given a hardware platform and a set of applications is typically divided into three steps: binding, routing, and scheduling. Binding describes the process of allocating a resource for a specific task, routing ensures that messages of communicating tasks are correctly delivered through the network, and scheduling assigns starting points for all tasks and communications so that no conflicts occur while executing applications.

By assigning worst-case execution times to tasks, as well as energy consumption and costs to resources, we are able to evaluate several quality criteria of a design point. We mainly focused on latency, i.e., a design point is better if all applications are finished in a shorter amount of time, energy consumption and hardware cost. These quality criteria are aggregated via a Pareto preference, i.e., a design point is better if it is at least as good in all criteria and strictly better in at least one when compared to another design point. Note that this preference might lead to a vast amount of optimal solutions since design points might be incomparable.

3 DSE using Hybrid ASP

In this work, our focus lay on developing exact and flexible methods using ASP technology for finding design points for complex system models, obtaining optimal design points, and enumerating and storing optimal design points.

In detail, in [2], we propose a novel ASPmT system synthesis approach. It supports more sophisticated system models, and makes use of tightly integrated background theories and partial solution checking. We present a comprehensive Hybrid ASP encoding of all aspects of system synthesis, i.e., binding, routing, scheduling. As underlying technology, we use the ASP system clingo [1] whose grounding and solving components allow for incorporating application- or theory-specific reasoning into ASP. In [3], we present a novel approach to a holistic system level DSE based on Hybrid ASP. DSE including feasibility check and optimization is performed directly within the solving process. To achieve that, we include additional background theories that concurrently guarantee compliance with hard constraints and perform the simultaneous optimization of several design objectives. Binding, routing, scheduling and design objectives are represented in a declarative fashion in one encoding. Experimental results show the applicability of our approach for large optimization problems of up to 170 tasks mapped to 3-dimensional hardware platforms.

References

1. M. Gebser, R. Kaminski, B. Kaufmann, M. Ostrowski, T. Schaub & P. Wanko (2016): Theory Solving Made Easy with Clingo 5 . In M. Carro & A. King, editors: Technical Communications of the Thirty-second International Conference on Logic Programming (ICLP’16) , OpenAccess Series in Informatics (OASIcs) 52, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 2:1-2:15, doi:10.4230/OASIcs.ICLP.2016.2.
2. K. Neubauer, P. Wanko, T. Schaub & C. Haubelt (2017): Enhancing symbolic system synthesis through ASPmT with partial assignment evaluation . In D. Atienza & G. Di Natale, editors: Proceedings of the Twentieth Conference on Design, Automation and Test in Europe (DATE’17) , IEEE Computer Society Press, pp. 306-309, doi:10.23919/DATE.2017.7927005.
3. K. Neubauer, P. Wanko, T. Schaub & C. Haubelt (2018): Exact Multi-Objective Design Space Exploration using ASPmT . In J. Madsen & A. Coskun, editors: Proceedings of the Twenty-first Conference on Design, Automation and Test in Europe (DATE’18) , IEEE Computer Society Press, pp. 257-260, doi:10.23919/DATE.2018.8342014.
4. A. Pimentel (2017): Exploring Exploration: A Tutorial Introduction to Embedded Systems Design Space Exploration . IEEE Design & Test 34(1), pp. 77-90, doi:10.1109/MDAT.2016.2626445.

---

LP Based Integration of Computing and Science Education in Middle Schools

Yuanlin Zhang (Texas Tech University)
Jianlan Wang (Texas Tech University)
Fox Bolduc (Texas Tech University)
William G Murray (Texas Tech University)

This is an extended abstract of our paper [1].

Introduction

There is consensus on the need of integrating computing, integral to the practice of all other STEM disciplines, in STEM teaching and learning in K-12 (Kindergarten to 12th grade in the US education system) (see, e.g., [2]). However, little is known about how best Computing can be taught and how to integrate it with STEM disciplines to improve STEM and Computing learning in K-12 in general and middle schools in particular. In this paper, we propose a Logic Programming (LP) based framework for integration, called LPK12 and report the study of the feasibility of LPK12.

LP-based Integration of Computing and STEM Teaching

LPK12 achieves a deep integration of Computing and STEM education by building computer models for STEM problems through Answer Set Programming (ASP) [3] -a modern LP paradigm. The integration consists of the following components. We will use food chain, a middle school science topic, as an running example.
• Problem description. Consider a food chain with carrots, rabbits, snakes and eagles. The problem description is centered around questions. Typical questions include "Q1: do eagles eat snakes?" and "Q2: what would happen to eagles if snakes become extinct?" Students are expected to review or learn food chains and how these questions can be answered.
• Modeling.
  • Identify objects in the problem and their kinds or sort. E.g.,

    #species = {eagle, snake, rabbit, carrot}.

  • Identify Relations among the objects for the problem. E.g., we introduce a relation of the form

    feedsOn(X,Y) which means that members of species X feed on those of species Y .

  • Extract knowledge from the problem and represent them as rules. E.g., a piece of knowledge is

    "rabbits feed on carrots," which is represented as

    feedsOn(rabbit,carrot).

LPK12 is based on the following arguments. First, LP has low floor and high ceiling [4]. It allows students to start developing computer models for interesting, non-trivial STEM problems after a very short introduction and yet it is a full-fledged programming paradigm. Second, LP facilitates a unified treatment of the fundamental skills and topics in STEM and Computing thanks to the fact that LP is based on discoveries and ideas of Logic which forms an important base for learning and problem solving in all STEM disciplines. The LP modeling methodology allows a natural and seamless connection of subject-matter concepts and reasoning to computer model development. Thirdly, middle school students are cognitively ready for LP based approaches. By Piaget, children at age 11 to 15 demonstrate substantial knowledge of natural language and the logical use of symbols related to abstract concepts. Finally, for STEM, LPK12 facilitates students to develop fundamental skills in Science and Computing.

LPK12 Facilitates STEM and Computing Learning

LPK12 is arguably able to facilitate students learning Science skills, such as asking questions and defining problems, constructing explanations, engaging in argumentation, and communicating information, as defined in next generation science standards (NGSS) [5]. For Computing, students will get abundant opportunities to learn and practice various levels of abstraction, problem solving , programming and communication as identified in the K-12 Computer Science Framework [6].

Related Work

Logic Programming Research and Its Use in Education. Logic Programming is a meeting point of Thinking, Logic and Computing [7]. It has been studied for teaching children since the 1980s [12] because of its declarativeness. Unfortunately, the strong procedural component of classical LP systems such as PROLOG has prevented LP from reaching a wider audience [8]. A major breakthrough in the last two decades is the establishment of Answer Set Programming [3] -a purely declarative LP paradigm. LPK12 is based on SPARC [9], an ASP with types. Programming Systems in K-12. The mainstream systems used in K-12 is based on visual programming environments such as Scratch. In contrast, SPARC is a text based programming language. Note also that major visual programming environments are based on imperative programming paradigm, other than declarative paradigms. Integration of Computing and STEM Teaching. A work closely related to LPK12 is the framework proposed in [10] which uses agent-based computation to integrate Computing and science. We also note ad-hoc integrations such as the work reported in mathematics [11].

Feasibility Study of LPK12

Participants and Context

This study took place in an elective course with the name STEM. The participants were one STEM teacher and her four sections of 96 6th-graders and three sections of 71 7th-graders in a middle school with 900 students located in a middle-south city in the United States.

LP Based Integration Modules and Implementation

We developed a chemistry module (periodic table) for 6th graders and physics module (motion) for 7th graders. Each module is implemented in 8 class sessions. Each class session is 50 minutes long and consists of one or several cycles. Each cycle consists of two components: concept understanding (5-10 minutes) and programming practices. The Computing content of both modules: introduction to Computing and computer models for problem solving; concepts of relations, facts, and queries; variables; and rules. The chemistry module covers the content of understanding of (the language of) periodic table, atom structure and relationship among atomic number, proton number, electron number and mass number of an atom. The physics module covers the concept of an object's motion relative to a reference object and the associate sub concepts.

Data Collection and Analysis

We administered pre- and post-surveys to examine the learning outcome, and carried out one post semi-structured group interview for each grade to gauge the students' feedback to their experience with the integration modules.

The pre- and pos-surveys contain multiple-choice questions assessing students' scientific content knowledge of interest and computer science skills. The science questions have been previously validated. Since LP is new in teaching Computing, the questions are designed by the researchers by following the guide in [4]. The questions from the pre- and post-surveys are substantially the same and vary only in different context.

The data on the background information of the students and the paired t-tests of assessments on science and Computing is provide in the original paper [1]. The interview results were also reported there.

Findings

Q1. How did the integration modules affect the students' learning?

The modules have helped most of the participating students make considerable progress in Computing. Similarly, the 7th graders' physics content knowledge increased significantly. However, the 6th graders' chemistry content knowledge does not have a statistically significant change. From the interviews, students show positive experience with programming and LP.

Q2. How the participants reflect on their experience with the LP based integration?

13 out of 15 interviewees thought that the modules were interesting. 14 out 15 interviewees believed that computing impacted science learning, and vice versa. Thus, the LP based integration of science and Computing is accepted by the students.

Conclusion

By our experience, the framework allows a rather straightforward development of the chemistry and physics modules. We conjecture that the development of modules for other topics in science (or STEM in general), based on our modules, will also be straightforward. Our survey data show that students' learning has been improved on physics and Computing (abstraction) significantly. Class observations and interviews show that students are doing well in the other aspects of Computing: programming and communication. Interviews also show the LP based integration is accepted by students: the modules are interesting and there is a positive impact of computing and science to each other. In summary, LP based integration seems to be promising in terms of the development and implementation of the two 8-session modules, the students' learning outcomes. There are some limitations in this preliminary study, for example, we did not measure students' development of problem solving capacity, a Computing practice, and we did not control other variables in our experiment.

Acknowledgment

We thank Michael Gelfond, Wendy Staffen, Jeremy Wagner, Michael Strong and Edna Parr for their help and support in this research. The presentation of this work at ICLP-2019 is supported by NSF grant DRL-1901704.

References

1. Zhang, Y., Wang, J., Bolduc, F., & Murray, W. G. (2019, May): LP Based Integration of Computing and Science Education in Middle Schools . In Proceedings of the ACM Conference on Global Computing Education (pp. 44-50). ACM. doi:10.1145/3300115.3309512.
2. NSF. (2018): STEM+C Program . https://www.nsf.gov/funding/pgm_summ.jsp? pims_id=505006, retrieved on October 10 2018.
3. Michael Gelfond and Yulia Kahl. (2014): Knowledge Representation, Reasoning, and the Design of Intelligent Agents . Cambridge University Press. doi:10.1017/CBO9781139342124.
4. SeymourPapert. (1980): Mindstorms: Children, computers, and powerful ideas. . Basic Books, Inc. doi:10.1145/1045071.1045074.
5. NGSS Lead States. (2006): Next generation science standards: For states, by states. . National Academies Press.
6. K-12 Computer Science Framework. (2017): K-12 Computer Science Framework. . http://www.k12cs.org. Retrieved on September 4 2018.
7. Robert Kowalski. (2014): Logic Programming. . Computational Logic, Volume 9 (Handbook of the History of Logic).
8. Patrick Mendelsohn, TRG Green, and Paul Brna. (1991): Programming languages in education: The search for an easy start. . In Psychology of programming. Elsevier, 175-200. doi:10.1016/B978-0-12-350772-3.50016-1.
9. Balai E., Gelfond M., Zhang Y. (2013): Towards Answer Set Programming with Sorts. . In: Cabalar P., Son T.C. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2013. doi:10.1007/978-3-642-40564-8_14.
10. Pratim Sengupta, John S Kinnebrew,Satabdi Basu,Gautam Biswas, and Douglas Clark. (2013): Integrating computational thinking with K-12 science education using agent-based computation: A theoretical framework. . Education and Information Technologies 18, 2 (2013), 351-380. doi:10.1007/s10639-012-9240-x.
11. Emmanuel Schanzer, Kathi Fisler, Shriram Krishnamurthi, and Matthias Felleisen. (2015): Transferring skills at solving word problems from computing to algebra through Bootstrap. . In Proceedings of the 46th ACM Technical symposium on computer science education. ACM, 616-621. doi:10.1145/2676723.2677238.
12. Robert A Kowalski. (1982): Logic as a computer language for children. . In Proceedings of ECAI. 2-10.

---

Strong Equivalence for Epistemic Logic Programs Made Easy: Extended Abstract

Wolfgang Faber (University of Klagenfurt, Austria)
Michael Morak (University of Klagenfurt, Austria)
Stefan Woltran (TU Wien, Vienna, Austria)

This is an extended abstract of the paper: Faber, W., Morak, M., Woltran, S.: Strong Equivalence for Epistemic Logic Programs Made Easy. In: Proc. AAAI. (2019)

Epistemic Logic Programs (ELPs) [4,5,8] are an extension of the established formalism of Answer Set Programming (ASP) (cf. e.g. [1]) with an epistemic negation operator $\mathbf{not}\,a$ that operates w.r.t. a set of answer sets, with the intended meaning that $\mathbf{not}\,a$ cannot be proven to be true in all answer sets.

An insteresting question in the world of ASP is that of strong equivalence between two ASP programs [7,9], that is, whether the two can always be replaced by one another in the context of a larger ASP program, without affecting the answer sets. In this paper, our aim is to study strong equivalence for ELPs w.r.t. the semantics defined in [8]. This problem has been already considered for ELPs (cf. e.g. [10,3]), but these studies generally do not deal with the semantics as defined in [8]. However, since this particular semantics is implemented in several of today's ELP solvers, we would like to specifically investigate strong equivalence for this setting, in the spirit of [9].

ELPs, as defined in [8], are (finite) sets of ELP rules of the form

$a_1\vee \cdots \vee a_k \leftarrow \ell_1, \ldots, \ell_m, \xi_1, \ldots, \xi_j, \neg \xi_{j + 1}, \ldots, \neg \xi_{n},$

where each $a_i$ is an atom, each $\ell_i$ is a literal, and each $\xi_i$ is an epistemic literal $\mathbf{not}\,\ell$, where $\ell$ is a literal. The semantics of ELPs are defined w.r.t. an epistemic guess, that is, a set of epistemic literals. From such a guess $\Phi$, an ELP $\Pi$ is first transformed into an epistemic reduct $\Pi^\Phi$ by replacing epistemic literals in $\Phi$ with $\top$ and all other ocurrances of epistemic negation with standard default negation (yielding an ASP program). We then say that the set of answer sets of $\Pi^\Phi$ is a world view iff each epistemic literal in $\Phi$ is satisfied by this set of answer sets, and each other epistemic literal is not. Two ELPs can then be defined to be (ordinarily) equivalent iff their (candidate) world views coincide.

In order to define strong equivalence for ELPs, we extend the ASP definition:

Definition 1 Two ELPs $\Pi_1$ and $\Pi_2$ are \emph{strongly equivalent} iff, for any other ELP $\Pi$, the two ELPs $\Pi_1 \cup \Pi$ and $\Pi_2 \cup \Pi$ are (ordinarily) equivalent.

To syntactically characterize this relation we make use of a so-called SE-function:

Definition 2 The SE-function ${\cal S}{\cal E}_\Pi(\cdot)$ of an ELP $\Pi$ maps epistemic guesses $\Phi$ for $\Pi$ to sets of SE-models as follows.

${\cal S}{\cal E}_\Pi(\Phi) = \left\{ % \begin{array}{@{}lr@{}} % \mathit{semods}(\Pi^\Phi) \qquad & \text{if } \Phi \text{ realizable in } \Pi\\ % \emptyset & \text{otherwise.} % \end{array} % \right.$

Here, $\mathit{semods}(\Pi)$ refers to the notion of SE-models of an ASP program $\Pi$ (cf. [9]), that is, the set of pairs $(X, Y)$, such that $Y$ is a model of an ASP program $\Pi$, and $X \subseteq Y$ is a model of the GL-reduct [6] of $\Pi$ w.r.t. $Y$. We say that an epistemic guess $\Phi$ is realizable in a set of SE-models, iff there is a subset of SE-models, such that the $Y$-component of each SE-model would form a world view w.r.t. $\Phi$.

We then show that the SE-function precisely characterizes strong equivalence:

Theorem 1 ELPs are strongly equivalent iff they have the same SE-function.

We also show that our notion of strong equivalence strictly generalizes strong equivalence for ASP. With the SE-function defined, we also establish relevant complexity results. Particularly interesting is the fact that the complexity of checking strong equivalence for ELPs remains the same as for ASP:

Theorem 2 Checking that two ELPs are strongly equivalent is $coNP$-complete.

We then show that our results can be used to precisely characterize the syntactic shape of tautological ELP rules, as well as to give syntacic conditions that precisely identify when one ELP rule subsumes another. For example, an ELP rule is tautological if an atom appears both un-negated and epistemically negated in its body. Our syntactic conditions for rule tautologies and rule subsumptions generalize similar syntactic conditions that exist for plain ASP [2].

As future work, we plan to apply our findings to find a normal form for ELPs, as was done for ASP in [2], and would also like to study weaker forms of equivalence for ELPs.

References

1.   Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92-103 (2011), https://doi.org/10.1145/2043174.2043195.
2.   Cabalar, P., Pearce, D., Valverde, A.: Minimal logic programs. In: Proc. ICLP. LNCS, vol. 4670, pp. 104-118. Springer (2007), https://doi.org/10.1007/978-3-540-74610-2_8.
3.   Fariñas del Cerro, L., Herzig, A., Su, E.I.: Epistemic equilibrium logic. In: Proc. IJCAI. pp. 2964-2970 (2015)
4.   Gelfond, M.: Strong introspection. In: Proc. AAAI. pp. 386-391 (1991)
5.   Gelfond, M.: Logic programming and reasoning with incomplete information. Ann. Math. Artif. Intell. 12(1-2), 89-116 (1994), https://doi.org/10.1007/BF01530762.
6.   Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R.A., Bowen, K.A. (eds.) Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, USA, August 15-19, 1988 (2 Volumes). pp. 1070-1080. MIT Press (1988)
7.   Lifschitz, V., Pearce, D., Valverde, A.: Strongly equivalent logic programs. ACM Trans. Comput. Log. 2(4), 526-541 (2001), < href="https://doi.org/10.1145/383779.383783">https://doi.org/10.1145/383779.383783.
8.   Shen, Y., Eiter, T.: Evaluating epistemic negation in answer set programming. Artif. Intell. 237, 115-135 (2016), https://doi.org/10.1016/j.artint.2016.04.004.
9.   Turner, H.: Strong equivalence made easy: nested expressions and weight constraints. TPLP 3(4-5), 609-622 (2003), https://doi.org/10.1017/S1471068403001819.
10.   Wang, K., Zhang, Y.: Nested epistemic logic programs. In: Proc. LPNMR. LNCS, vol. 3662, pp. 279-290. Springer (2005), https://doi.org/10.1007/11546207_22.

---

Founded Semantics and Constraint Semantics of Logic Rules: An Overview

Yanhong A. Liu (Computer Science Department, Stony Brook University)
Scott D. Stoller (Computer Science Department, Stony Brook University)

Logic rules and inference are fundamental in computer science and have been a subject of significant study, especially for complex rules that involve recursion and unrestricted negation and quantifications. Many different semantics and computation methods have been proposed. Even those used in many Prolog-based systems and Answer Set Programming systems—negation as failure, well-founded semantics (WFS), and stable model semantics (SMS)—have subtle implications and differ significantly.

In practice, different semantics may be useful under different assumptions about the facts, rules, and reasoning used. For example, an application may have complete information about some predicates, i.e., sets and relations, but not other predicates. Capturing such situations is important for increasingly larger and more complex applications. Any semantics that is based on a single set of assumptions for all predicates cannot best model such applications.

Liu and Stoller [1] describes a simple new semantics for logic rules, founded semantics, and its straightforward extension to another simple new semantics, constraint semantics. The new semantics support unrestricted negation (both stratified and non-stratified), as well as unrestricted combinations of existential and universal quantifications. They allow specifying appropriate assumptions about each predicate.

Certain or uncertain. Founded semantics and constraint semantics first allow a predicate to be declared certain (i.e., each assertion of the predicate has one of two values: true (T), false (F)) or uncertain (i.e., each assertion of the predicate has one of three values: T, F, undefined (U)) when there is a choice.

• For a certain predicate, everything T must be given or inferred by following the rules, and the rest are F, in both founded semantics and constraint semantics.
• For an uncertain predicate, everything T or F must be given or inferred, and the rest are U in founded semantics. Constraint semantics then extends everything U to be combinations of T and F that satisfy all the rules and facts as constraints.

Complete or not. Founded semantics and constraint semantics then allow an uncertain predicate that is in the conclusion of a rule to be declared complete, i.e., all rules with that predicate in the conclusion are given.

• If a predicate is complete, then completion rules are added to define the negation of the predicate explicitly using the negation of the hypotheses of all given rules and facts of that predicates.
• Completion rules, if any, and given rules are used together to infer everything T and F. The rest are U in founded semantics, and are combinations of T and F in constraint semantics as described above.

Founded semantics and constraint semantics unify the core of previous semantics and have three main advantages:

1. They are expressive and intuitive, by allowing assumptions about predicates and rules to be specified explicitly, by including the choice of uncertain predicates to support common-sense reasoning with ignorance, and by adding explicit completion rules to define the negation of predicates.
2. They are completely declarative. Founded semantics takes the given rules and completion rules as recursive definitions of the predicates and their negation, and is simply the least fixed point of the recursive functions. Constraint semantics takes the given rules and completion rules as constraints, and is simply the set of all solutions that are consistent with founded semantics.
3. They relate cleanly to prior semantics, including stratified semantics, first-order logic, Fitting semantics (also called Kripke-Kleene semantics), and supported models, as well as WFS and SMS, by precisely capturing corresponding assumptions about the predicates and rules.
Additionally, founded semantics can be computed in linear time in the size of the ground program, as opposed to quadratic time for WFS.

Closed or not. Founded semantics and constraint semantics can be extended to allow an uncertain, complete predicate to be declared closed, i.e., an assertion of the predicate is made F, called self-false, if inferring it to be T (respectively F ) using the given rules and facts requires assuming itself to be T (respectively F).

• Determining self-false assertions is similar to determining unfounded sets in WFS. Repeatedly computing founded semantics and self-false assertions until a least fixed point is reached yields WFS.
• Among combinations of T and F values for assertions with U values in WFS, removing each combination that has self-false assertions that are not already F in that combination yields SMS.

Liu and Stoller [1] includes additional motivation and discussion, formal definitions of founded semantics and constraint semantics, theorems relating them with all of the other semantics mentioned above, and extensions of the language and semantics to allow unrestricted combinations of existential and universal quantifications as well as negation, conjunction, and disjunction in hypotheses.

Acknowledgements. This work was supported in part by NSF under grants CCF-1414078, CNS-1421893, IIS-1447549, CCF-1248184, CCF-0964196, and CCF-0613913; and ONR under grants N000141512208 and N000140910651.

References

1. Liu, Y.A., Stoller, S.D.: Founded semantics and constraint semantics of logic rules. In: Proceedings of the International Symposium on Logical Foundations of Computer Science. pp. 221-241. Springer (2018). doi:10.1007/978-3-319-72056-2_14.

---

Weight Learning in a Probabilistic Extension of Answer Set Programs (Extended Abstract)

Joohyung Lee (School of Computing, Informatics and Decision Systems Engineering Arizona State University, Tempe, AZ, USA)
Yi Wang (School of Computing, Informatics and Decision Systems Engineering Arizona State University, Tempe, AZ, USA)

This is an extended abstract of the paper [2], which was presented at the 16th International Conference on Principles of Knowledge Representation and Reasoning (KR 2018).

LPMLN [1] is a probabilistic extension of answer set programs with the weight scheme derived from Markov Logic [3]. The weight associated with each LPMLN rule asserts how important the rule is in deriving "soft" stable models, which do not necessarily satisfy all rules in the program, but the more rules with the bigger weights they satisfy, the bigger probabilities they get. The weights of the rules can be manually specified by the user, which could be challenging when the program becomes more complex, so a systematic assignment of weights is more desirable. The paper [2] presents a way to learn the weights automatically from the observed data. It first presents the concept of weight learning in LPMLN and a few learning methods for LPMLN derived from learning in Markov Logic. Weight learning in LPMLN is to find the weights of the rules in the LPMLN program such that the likelihood of the observed data according to the LPMLN semantics is maximized, which is commonly known as Maximum Likelihood Estimation (MLE) in the practice of machine learning.

Formally, given a parameterized LPMLN program \(\hat{\Pi}\) and a ground formula \({O}\) (often in the form of conjunctions of literals) called observation or training data, the LPMLN parameter learning task is to find the values w of parameters such that the probability of 0 under the LPMLN program \(\Pi\) is maximized. In other words, the learning task is to find \[ \underset{{\bf w}}{\rm argmax}\ P_{\hat{\Pi}({\bf w})}(O). \] The partial derivative of \(ln P_{\Pi}(I)\) w.r.t. \(w_i (\ne \alpha)\) is \[ \frac{\partial ln P_{\Pi}(I)}{\partial w_i} = -n_i(I) + \underset{J\in SM[\Pi]}{\sum}P_{\Pi}(J)n_i(J) = -n_i(I) + \underset{J\in SM[\Pi]}E[n_i(J)] \] where \(n_i(I)\) is the the number of ground instances of rule \(R_i\) that is false in \(I\) and \(SM[\Pi]\) denotes the set of "soft" stable models. \(E_{J\in SM[\Pi]} [n_i(J)]= {\sum}_{J\in SM[\Pi]}P_{\Pi}(J)n_i(J)\) is the expected number of false ground rules obtained from \(R_i\). Since the log-likelihood of \(\Pi_\Pi(O)\) is a concave function of the weights, any local maximum is a global maximum, and maximizing \(P_\Pi(I)\) can be done by the standard gradient ascent method by updating each weight \(w_i\) by \[ w_i+\lambda\cdot (-n_i(I) + \underset{J\in SM[\Pi]}{E}[n_i(J)]) \] until it converges.

However, similar to Markov Logic, computing \(E_{J\in SM[\Pi]}[n_i(J)]\) is intractable [3]. The paper presents an MCMC sampling method called MC-ASP to find its approximate value.

The following is a simple example illustrating the usefulness of LPMLN weight learning. Consider an (unstable) communication network, where each node represents a signal station that sends and receives signals. A station may fail, making it impossible for signals to go through the station. The following LPMLN rules define the connectivity between two stations X and Y in session T.

  connected(X,Y,T) :- edge(X,Y), not fail(X,T), not fail(Y,T).
  connected(X,Y,T) :- connected(X,Z,T), connected(Z,Y,T).

A specific network can be defined by specifying edge relations, such as edge(1,2).

Suppose we have data showing the connectivity between stations in several sessions. Based on the data, we could make decisions such as which path is most reliable to send a signal between the two stations. Under the LPMLN framework, this can be done by learning the weights representing the failure rate of each station. For example, we write the following rules whose weights w\((i)\) are to be learned:

   @w(1) fail(1, T).    ...     @w(10) fail(10, T).

In summary, the work presented relates answer set programming to learning from data, which has been largely under-explored. Via LPMLN, learning methods developed for Markov Logic can be adapted to find the weights of rules under the stable model semantics, utilizing answer set solvers for performing MCMC sampling. Rooted in the stable model semantics, LPMLN learning is useful for learning parameters for programs modeling knowledge-rich domains. Unlike MC-SAT for Markov Logic, MC-ASP allows us to infer the missing part of the data guided by the stable model semantics. Overall, the work paves a way for a knowledge representation formalism to embrace machine learning methods.

References

1. Joohyung Lee & Yi Wang (2016): Weighted Rules under the Stable Model Semantics. In: Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 145-154.
2. Joohyung Lee & Yi Wang (2018): Weight Learning in a Probabilistic Extension of Answer Set Programs. In: Proceedings of International Conference on Principles of Knowledge Representation and Reasoning (KR), pp. 22-31.
3. Matthew Richardson & Pedro Domingos (2006): Markov logic networks. Machine Learning 62(1-2), pp. 107-136, doi:10.1007/s10994-006-5833-1

---

Strong Equivalence for LPMLN Programs

Man Luo (Arizona State University)

Introduction

I study the concept of strong equivalence in \(LP^{MLN}\) and show that the verification of strong equivalence in \(LP^{MLN}\) can be reduced to equivalence checking in classical logic plus weight consideration.The result allows us to leverage an answer set solver for checking strong equivalence in \(LP^{MLN}\). Furthermore, this study also suggests us a few reformulations of the \(LP^{MLN}\) semantics using choice rules, logic of here and there, and the second-order logic.

\(LP^{MLN}\) is a probabilistic extension of answer set programs with the weight scheme adapted from Markov Logic. An \(LP^{MLN}\) program defines the probability distribution over all ``soft'' stable models, which do not necessarily satisfy all rules in the program, but the more rules with the bigger weights they satisfy, the bigger their probabilities.

Informally speaking, logic programs \(P\) and \({Q}\) are strongly equivalent if, given any program \({R}\), programs \({P} \cup {R}\) and \({Q} \cup {R}\) have the same stable models. However, because of the semantic differences, strong equivalence for answer set programs does not simply carry over to \(LP^{MLN}\). First, weights play a role. Even for the same structure of rules, different assignments of weights make the programs no longer strongly equivalent. Also, due to the fact that soft stable models do not have to satisfy all rules, strongly equivalent answer set programs do not simply translate to strongly equivalent \(LP^{MLN}\) programs.

Background and result

An \(LP^{MLN}\) program is a finite set of weighted formulas \(w: R\) where \(R\) is a propositional formula and \(w\) is a real number or \(\alpha\) for denoting the infinite weight. For any \(LP^{MLN}\) program \(F\) and any set \(X\) of atoms, \(\overline {F} \) denotes the set of usual (unweighted) formulas obtained from \({F}\) by dropping the weights, and \({F}_X\) denotes the set of \(w: R\) in \({F}\) such that \(X \models R\). Given an \(LP^{MLN}\) program \({F}\), \(X\) is a soft stable model of \({F}\) if \(X\) is a (standard) stable model of \({{F}_X}\). \(SM[{F}]\) denotes the set of soft stable models. By \({TW}({F})\) we denote the expression \(exp({\sum\limits_{ w:R \in {F}} w})\). For any interpretation \(X\), the weight of an interpretation \(X\), denoted \(W_{{F}}(X)\), is defined as \[ W_{{F}}(X) = \begin{cases} {TW}({F_X}) & \text{if \(X \in SM[{F}]\)}; \\ 0 & \text{otherwise}, \end{cases} \] and the probability of \(X\), denoted \(P_{F}(X)\), is defined as \[ P_{F}(X) = \lim\limits_{\alpha\to\infty} \frac{W_{F}(X)}{\sum\limits_{Yn {\rm SM}[{F}]}{W_{F}(Y)}}. \]

Definition:

\(LP^{MLN}\) programs \({F}\) and \({G}\) are called strongly equivalent to each other if, for any \(LP^{MLN}\) program \({H}\), \[ P_{{F}\cup {H}}(X) = P_{{G}\cup {H}}(X) \] for all interpretations \(X\).

The following theorem shows a characterization of strong equivalence that does not need to consider adding all possible \(LP^{MLN}\) program \({H}\), which can be reduced to equivalence checking in classical logic plus weight checking. By \({F}^X\), we denote the reduct of \({F}\) obtained from \({F}\) by replacing every maximal subformula of \({F}\) that is not satisfied by \(X\) with \(\bot\).

Theorem:

For any \(LP^{MLN}\) programs \({F}\) and \({G}\), program \({F}\) is strongly equivalent to \({G}\) if and only if there is a w-expression \(c\) such that for every interpretation \(X\),

1. \(TW({F}_X) = c \times TW({G}_X)\), and
2. \(({{F}_X})^X\) and \(({{G}_X})^X\) are classically equivalent.
where \(w\)-expression is in the form of \(e^{c_1+c_2\alpha}\).
Example: Consider two programs
F:
\(0: \neg a \)
\(2: b \leftarrow a \)
G:
\(2: \neg a \lor b \)
\(1: a\lor \neg a \)
\(3: a \leftarrow \neg \neg a\)
Programs \({F}\) and \({G}\) are strongly equivalent to each other. The following table shows \( F\) and \( G\) statisfy two conditions in Theorem.



\(X\)	\(TW(F_X)\)	\(TW(G_X)\)	\((\overline{F_X})^{X}\)	\((\overline{G_X})^{X}\)
\(\phi\)	\(e^5\)	\(e^3\)	\(\top\)	\(\top\)
\(a\)	\(e^3\)	\(e^1\)	\(a\)	\(a\)
\(b\)	\(e^5\)	\(e^3\)	\(\top\)	\(\top\)
{a, b}	\(e^5\)	\(e^3\)	\(a \land b\)	\(a \land b\)

From the first and the second column, it is easy to see that \(TW({{F}_X}) = e^2 \times TW({G}_X)\), so the first condition in Theorem is satisfied. The third and forth column show that the second condition in Theorem is satisfied, so \(LP^{MLN}\) program \({F}\) and \({G}\) are strongly equivalent.

Conclusion

The study shows that checking strong equivalence for \(LP^{MLN}\) programs is no harder than the checking for answer set programs, and we can leverage an answer set solver for checking strong equivalence in \(LP^{MLN}\).

---