Published: 19th September 2019 DOI: 10.4204/EPTCS.306 ISSN: 20752180 
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:
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 realworld 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:
General ChairsThree kinds of submissions were accepted:
ICLP implemented the hybrid publication model used in all recent editions of the conference, with journal papers and Technical Communications (TCs), following a decision made in 2010 by the Association for Logic Programming. Papers of the highest quality were selected to be published as rapid publications in 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 shortlisted 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:
Hassan AitKaci  Mario Alviano  Roman Bartak  Rachel BenEliyahuZohary 
Bart Bogaerts  Gerhard Brewka  Pedro Cabalar  Michael Codish 
Stefania Costantini  Marina De Vos  Agostino Dovier  Thomas Eiter 
Wolfgang Faber  Fabio Fioravanti  Andrea Formisano  John Gallagher 
Martin Gebser  Michael Gelfond  Michael Hanus  Amelia Harrison 
Manuel Hermenegildo  Giovambattista Ianni  Daniela Inclezan  Katsumi Inoue 
Tomi Janhunen  Angelika Kimmig  Ekaterina Komendantskaya  Vladimir Lifschitz 
Evelina Lamma  Joohyung Lee  Nicola Leone  Yanhong Annie Liu 
Fred Mesnard  Jose F. Morales  Emilia Oikarinen  Carlos Olarte 
Magdalena Ortiz  Mauricio Osorio  Barry O'Sullivan  Simona Perri 
Enrico Pontelli  Ricardo Rocha  Alessandra Russo  Orkunt Sabuncu 
Chiaki Sakama  Torsten Schaub  Guillermo R. Simari  Theresa Swift 
Francesca Toni  Paolo Torroni  Tran Cao Son  Alicia Villanueva 
Kewen Wang  Jan Wielemaker  Stefan Woltran  Fangkai Yang 
Roland Yap  JiaHuai You  Zhizheng Zhang 
The Program Committee members of the Applications track were:
Chitta Baral  Alex Brik  Francesco Calimeri  Xiaoping Chen 
Federico Chesani  Martín Diéguez  Gerhard Friedrich  Gopal Gupta 
Jianmin Ji  Gabriele KernIsberner  Zeynep Kiziltan  Viviana Mascardi 
Yunsong Meng  Francesco Ricca  Mohan Sridharan  David Warren 
Shiqi Zhang  NengFa Zhou 
The Program Committee members of the Special Session: Women in Logic Programming were:
Elvira Albert  Stefania Costantini  Ines Dutra  Daniela Inclezan 
Ekaterina Komendantskaya  Simona Perri  Francesca Toni 
The external reviewers were:
Van Nguyen  Bernardo Cuteri  Dennis Dams  Anna Schuhmann 
Alberto Policriti  Jessica Zangari  Vítor Santos Costa  Arash Karimi 
Joxan Jaffar  Michael Frank  Roland Kaminski  Javier Romero 
Jose Luis Carballido  Christopher Kane  Emanuele De Angelis  Isabel GarciaContreras 
José Abel Castellanos Joo  Wolfgang Dvorak  Vitaly Lagoon  Jannik Dreier 
Philipp Wanko  Marco Gavanelli  Emanuel Sallinger  Weronika T. Adrian 
Wanwan Ren  Kinjal Basu  Patrick Kahl  Marco Alberti 
Gianluca Amato  Juan Carlos Nieves  Joaquin Arias  Miguel Areias 
Konstantin Schekotihin  Farhad Shakerin  Nada Sharaf  Christoph Redl 
Yuanlin Zhang  Yi Tong  K. Tuncay Tekle  Saksham Chand 
Yan Zhang  Jessica Zangari 
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, logicbased 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, cochairs, members of the program committee and the organizing team that made the Doctoral Consortium greatly successful.
The DC Program Committee members were:
Carmine Dodaro  Cristina Feier  Ekaterina Komendantskaya  Fabio Fioravanti 
Francesco Ricca  Frank Valencia  Jorge Fandino  Jose F. Morales 
Marco Maratea  Martin Gebser  Michael Gelfond 
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, EditorinChief of TPLP. Also, to the staff at Cambridge University Press for their assistance. We would also like to thank Rob van Glabbeek, EditorinChief 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.) 
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 inputoutput behavior, allowing one to symbolically explain the decisions made by these numeric classifiers.
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 logicbased 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 spinoff company of University of Calabria, and has been successfully used in several realworld 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 serverlike platform. Then, we focus on the description of some industrylevel 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 ASPbased technologies in the modern AI spring.
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 humaninterpretable abstractions. In this talk, I present the notion of a Reward Machine, an automatabased structure that provides a normal form representation for reward functions. Reward Machines can be used natively to specify complex, nonMarkovian rewardworthy behavior. Furthermore, a variety of compelling humanfriendly (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 partiallyobservable environments. By exposing reward function structure, Reward Machines enable rewardfunctiontailored reinforcement learning, including tailored reward shaping and Qlearning. Experiments show that such rewardfunctiontailored algorithms significantly outperform stateoftheart (deep) RL algorithms, solving problems that otherwise can't reasonably be solved and critically reducing the sample complexity.
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 nonground 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 humanperformed optimizations. This talk will present PROJECTOR and considered experimental analysis in great detail.
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.
Resource allocation poses unique challenges ranging from load balancing in heterogeneous environments to privacy concerns and various servicelevel agreements. In this tutorial, we highlight industrial applications from distinct problem domains that span both extremes of the optimization landscape; operational decision making in realtime and resource provisioning for future considerations. Motivated by realworld 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 largescale 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.
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, dDNNFs, 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 treeshaped 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 highlevel 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 highlevel reasoning about their firstorder structure to exploit symmetry and exchangeability, which can also be done within the probabilistic circuit framework.
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 overapproximate 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 interpretationbased analysis, a crucial issue is the tradeoff between cost and accuracy, and thus research in new abstract domains, widenings, fixpoints, etc., often requires studying this tradeoff. 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 adhoc 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 interpretationbased 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 setbased 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 interpretationbased analyses of a whole program, that is, distances in the space of ANDOR 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 ANDOR 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 interpretationbased analyses of a whole program, by just calculating the distances between the representation of those analyses as ANDOR 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 ANDOR trees).
Finally, we implement the proposed distances within the CiaoPP framework (Hermenegildo et al. 2005) and apply them to study the accuracycost tradeoff of different sharingrelated (C)LP analyses over a number of benchmarks and a real program. The domains sharefree, share, def, and sharefree 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 apriori 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.
Casso, I., J. F. Morales, P. LopezGarcia, and M. V. Hermenegildo. 2019. ''Computing Abstract Distances in Logic Programs.'' CLIP2/2019.0. The CLIP Lab, IMDEA Software Institute; T.U. Madrid. http://arxiv.org/abs/1907.13263.
Hermenegildo, M., G. Puebla, F. Bueno, and P. Lopez Garcia. 2005. ''Integrated Program Debugging, Verification, and Optimization Using Abstract Interpretation (and The Ciao System Preprocessor).'' Science of Computer Programming 58 (12): 11540.
This document is an extended abstract of Technical Report CLIP2/2019.0 (Casso et al. 2019). Research partially funded by MINECO project TIN201567522C31R TRACES and Comunidad de Madrid project S2018/TCS4339 BLOQUESCM, cofunded by EIE Funds of the European Union.
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 agreedupon 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 discretestatebased 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 wellknown 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 counterintuitive 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 wellknown 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 nondeterminism, timedependent 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 [1314], 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. selfdriving cars, Internet of Things and digital twin applications, and cyberphysical security systems).
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 complexityaware test execution mechanism. Testcase 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
(3colorability). 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).

Figure 1: Example of usage of the test annotation language with a program written in ASPCore2 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 testcase 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 complexityaware 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 annotationbased test
specification language, as well as the execution mechanism are
implemented as part of a webbased development environment called
ASPWIDE. It can be installed as a standalone application in any
computer with a modern (javascript enabled) web browser and Java 8
installed. ASPWIDE can be downloaded from:
http://www.mat.unical.it/ricca/asptesting/aspwide_1.0beta4.zip,
and the sources of the environment are distributed under GPL licence.
Onofrio Febbraro, Nicola Leone, Kristian Reale & Francesco Ricca (2011): Unit Testing in ASPIDE. In: INAP/WLP, Springer, Berlin, Heidelberg, pp. 345364, doi:10.1007/9783642415241_21.
Onofrio Febbraro, Kristian Reale & Francesco Ricca (2011): ASPIDE: Integrated Development Environment for Answer Set Programming. In: LPNMR, Springer, Berlin, Heidelberg, pp. 317330, doi:10.1007/9783642208959_37.
Marina De Vos, Doga Gizem Kisa, Johannes Oetsch, Jörg Pührer & Hans Tompits (2012): Annotating answerset programs in LANA. In: TPLP, pp. 619637, doi:10.1017/S147106841200021X.
Steven Fraser, Kent L. Beck, Bill Caputo, Tim Mackinnon, James Newkirk & Charlie Poole (2003): Test Driven Development (TDD). XP Springer, Berlin, Heidelberg, pp. 459462, doi:10.1007/3540448705_84.
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 resourcerelated specifications, and detection of performance bugs, as well as helping developers make resourcerelated 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 userdefinable 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) multicore 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 welldeveloped 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 AndParallelism (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 AndParallelism 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
metapredicate 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 closedform 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 andparallel 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 upperbound 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.
M. Klemen, P. LópezGarcía, J. Gallagher, J. F. Morales, and M. V. Hermenegildo. 2019. "Towards a General Framework for Static Cost Analysis of Parallel Logic Programs." CLIP1/2019.0. The CLIP Lab, IMDEA Software Institute; T.U. Madrid. http://arxiv.org/abs/1907.13272.
This document is an extended abstract of Technical Report CLIP1/2019.0 (Klemen et al. 2019). Research partially funded by MINECO project TIN201567522C31R TRACES and Comunidad de Madrid project S2018/TCS4339 BLOQUESCM, cofunded by EIE Funds of the European Union.
The concept of PreMappable (PreM) constraints in recursive queries has made possible
(i) the declarative expression of classical algorithms in Datalog and other logicbased 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, NonMonotonic Semantics
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 SQL2003 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/rightlinear 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, wellfounded models and stable models.
On the other hand, concise expression and efficient support for a wide range of polynomial time
algorithms, while keeping a stratificationbased formal semantics, was made possible by the recent introduction of
premappable 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 postconstraints 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) nonmonotonic 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 specialpurpose graph languages and systems as has been demonstrated in the recently proposed work [6],
which addresses this area of weakness of the SQL2003 compliant DBMSs.
In order to realize the significant potential offered by PreM,
the concept must be wellunderstood 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.
In the example below, the predicate ${\tt path(X,Y,D)}$ is defined by the nonrecursive rule $r_{1.1}$,
which will be called an exit rule, and the recursive rule $r_{1.2}$. $r_{1.3}$ is the final postcondition 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 groupby argument and ${\tt D}$ is the cost argument.
(The groupby 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 rewriting $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 perfectmodel 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 equivalencepreserving [2] and more efficient since the program below reaches the minimal fixpoint in finite number of steps.
Whenever this equivalencepreserving transformation holds, we say the given constraint $\gamma$ is PreMappable (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.
min
of these $\tt Dxz$ values, thereby eventually having $T(I)= T(\gamma(I))$ i.e. $\gamma$ is iPreM in this case.
min
and max
constraints in recursive queries. Due to PreM, recursive queries
with extrema can now be used to provide efficient scalable support of advanced applications [4] in both Datalog and SQL systems. The
use of aggregates in these systems is not restricted to just min
and max
: indeed,
count
and sum
can be expressed via the application of
max
to their monotonic versions [7]. Furthermore, the benefits of PreM
in expediting the execution of queries in data stream management systems and in parallel and distributed
systems have been respectively studied in [3] and [5]
Answer Set Programming (ASP) [3, 9] is a declarative programming paradigm proposed in the area of nonmonotonic 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 onetoone 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 preprocessing means aiming at making performance less encodingdependent; 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 heuristicguided 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 IDLV [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 divideandconquer 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 Heuristicguided 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 IDLV 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 variablefree 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%.
SDRL: Interpretable and Dataefficient Deep Reinforcement Learning Leveraging Symbolic Planning
Deep reinforcement learning (DRL) has gained great success by learning directly from highdimensional sensory inputs ([1]), yet is criticized for the lack of dataefficiency and interpretability. Especially, interpretability of subtasks is critical in hierarchical decisionmaking since it enhances the transparency of blackboxstyle DRL methods and helps the RL practitioners to understand the highlevel behavior of the system better ([2]).
To address the aforementioned issues, we propose the symbolic deep reinforcement learning (SDRL) framework in this work. Specifically, ASPbased logic programming is used for highlevel symbolic planning, while DRL can be utilized to learn lowlevel control policy. In addition, there is an intermediate metalearner that evaluates the learning performance and improves the goal of the planning. As a result, those three components crossfertilize 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, datadriven subtask learning, and subtask evaluation. Meanwhile, experiments validate that interpretability can be achieved through explicitly encoding declarative knowledge and learning into humanreadable subtasks, and also dataefficiency can be improved through automatic selecting and learning control policies of modular subtasks.
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, commercialofftheshelf (COTS) software products exist to manage Digital Forensics cases. Such products are usually workflowdriven, and provide mechanisms for information access, for search and data visualization. However, support for the effective aggregation and organization of useful evidence is simply nonexistent. 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 longterm perspective is in fact to construct a toolkit 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 proofbased 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 computationallogicbased 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 stateoftheart inference engines.
In this paper, we make a first step in the aboveoutlined direction. In fact, we illustrate, as a proof of concept, the transposition of a number of sample common investigation cases into Answer Set Programming (ASP), and we devise in general terms a methodology for doing so. We choose on purpose to translate some sample investigation problems into wellknown combinatorial problems and to use for demonstration existing ASP encodings, in analogy to the reduction methodology that is customary in complexity theory. This is because our intent here was not that of devising new code, rather it was exactly that of demonstrating how sample cases might be reduced to wellknown computational problems. These encodings and many others might in perspective constitute elements to exploit, combine and customize in the envisioned Decision Support System.
Answer Set Programming (ASP [8]) has become a popular approach to solving knowledgeintense 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 finegrained 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 Yaleshootingscenario, 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 HereandThere(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 threevalued. 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 nonmonotonic counterpart of LDL$_f$[5], being in an analogous relationship as classical and equilibrium logic, or SAT and ASP, respectively.
^{1} The same consideration led to GOLOG [7] in the context of the situation calculus.
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 followup 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, metaheuristic algorithms were used almost exclusively, but they do not guarantee optimality and are ineffective for finding feasible designs in highly constrained environments. ASPbased 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.
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 manycore SoCs) described at the electronic system level. Here, applications are defined as tasklevel 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 worstcase 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.
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 theoryspecific 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 3dimensional hardware platforms.
This is an extended abstract of our paper [1].
#species = {eagle, snake, rabbit, carrot}.
feedsOn(X,Y) which means that members of species X feed on those of species Y .
"rabbits feed on carrots," which is represented as
feedsOn(rabbit,carrot).
The pre and possurveys contain multiplechoice 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 postsurveys are substantially the same and vary only in different context.
The data on the background information of the students and the paired ttests of assessments on science and Computing is provide in the original paper [1]. The interview results were also reported there.
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
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 socalled SEfunction:
Definition 2 The SEfunction ${\cal S}{\cal E}_\Pi(\cdot)$ of an ELP $\Pi$ maps epistemic guesses $\Phi$ for $\Pi$ to sets of SEmodels as follows.
Here, $\mathit{semods}(\Pi)$ refers to the notion of SEmodels 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 GLreduct [6] of $\Pi$ w.r.t. $Y$. We say that an epistemic guess $\Phi$ is realizable in a set of SEmodels, iff there is a subset of SEmodels, such that the $Y$component of each SEmodel would form a world view w.r.t. $\Phi$.
We then show that the SEfunction precisely characterizes strong equivalence:
Theorem 1 ELPs are strongly equivalent iff they have the same SEfunction.
We also show that our notion of strong equivalence strictly generalizes strong equivalence for ASP. With the SEfunction 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 unnegated 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.
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 Prologbased systems and Answer Set Programming systems—negation as failure, wellfounded 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 nonstratified), 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.
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.
Founded semantics and constraint semantics unify the core of previous semantics and have three main advantages:
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 selffalse, if inferring it to be T (respectively F ) using the given rules and facts requires assuming itself to be T (respectively F).
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 CCF1414078, CNS1421893, IIS1447549, CCF1248184, CCF0964196, and CCF0613913; and ONR under grants N000141512208 and N000140910651.
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 loglikelihood 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 MCASP 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 underexplored. 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 knowledgerich domains. Unlike MCSAT for Markov Logic, MCASP 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.
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 secondorder 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.
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 wexpression \(c\) such that for every interpretation \(X\),
\(0: \neg a \)
\(2: b \leftarrow a \)
\(2: \neg a \lor b \)
\(1: a\lor \neg a \)
\(3: a \leftarrow \neg \neg a\)
\(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.
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}\).