The most advanced implementation of adaptive constraint processing with Constraint Handling Rules (CHR) allows the application of intelligent search strategies to solve Constraint Satisfaction Problems (CSP). This presentation compares an improved version of conflict-directed backjumping and two variants of dynamic backtracking with respect to chronological backtracking on some of the AIM instances which are a benchmark set of random 3-SAT problems. A CHR implementation of a Boolean constraint solver combined with these different search strategies in Java is thus being compared with a CHR implementation of the same Boolean constraint solver combined with chronological backtracking in SICStus Prolog. This comparison shows that the addition of “intelligence” to the search process may reduce the number of search steps dramatically. Furthermore, the runtime of their Java implementations is in most cases faster than the implementations of chronological backtracking. More specifically, conflict-directed backjumping is even faster than the SICStus Prolog implementation of chronological backtracking, although our Java implementation of CHR lacks the optimisations made in the SICStus Prolog system.

Efficient decision-making over continuously changing data is essential for many application domains such as cyber-physical systems, industry digitalization, etc. Modern stream reasoning frameworks allow one to model and solve various real-world problems using incremental and continuous evaluation of programs as new data arrives in the stream. Applied techniques use, e.g., Datalog-like materialization or truth maintenance algorithms to avoid costly re-computations, thus ensuring low latency and high throughput of a stream reasoner. However, the expressiveness of existing approaches is quite limited and, e.g., they cannot be used to encode problems with constraints, which often appear in practice. In this paper, we suggest a novel approach that uses the Conflict-Driven Constraint Learning (CDCL) to efficiently update legacy solutions by using intelligent management of learned constraints. In particular, we study the applicability of reinforcement learning to continuously assess the utility of learned constraints computed in previous invocations of the solving algorithm for the current one. Evaluations conducted on real-world reconfiguration problems show that providing a CDCL algorithm with relevant learned constraints from previous iterations results in significant performance improvements of the algorithm in stream reasoning scenarios.

For some computational problems (e.g., product configuration, planning, diagnosis, query answering, phylogeny reconstruction), computing a set of similar/diverse solutions may be desirable for better decision-making. With this motivation, we have studied several decision/optimization versions of this problem in the context of Answer set programming (ASP), analyzed their computational complexity, and introduced offline/online methods to compute similar/diverse solutions of such computational problems with respect to a given distance function. All these methods rely on the idea of computing solutions to a problem by means of finding the answer sets for an ASP program that describes the problem. The offline methods compute all solutions of a problem in advance using the ASP formulation of the problem with an existing ASP solver, like clasp, and then identify similar/diverse solutions using some clustering methods (possibly in ASP as well). The online methods compute similar/diverse solutions of a problem following one of the three approaches: by reformulating the ASP representation of the problem to compute similar/diverse solutions at once using an existing ASP solver; by computing similar/diverse solutions iteratively (one after the other) using an existing ASP solver; by modifying the search algorithm of an ASP solver to compute similar/diverse solutions incrementally. All these methods are sound; the offline method and the first online method are complete whereas the others are not. We have modified clasp to implement the last online method and called it clasp-nk. In the first two online methods, the given distance function is represented in ASP; in the last one, however, it is implemented in C++. We have shown the applicability and the effectiveness of these methods using clasp or clasp-nk on two sorts of problems with different distance measures: on a real-world problem in phylogenetics (i.e., reconstruction of similar/diverse phylogenies for Indo-European languages), and on several planning problems in a well-known domain (i.e., Blocks World). We have observed that in terms of computational efficiency (both time and space), the last online method outperforms the others; also, it allows us to compute similar/diverse solutions when the distance function cannot be represented in ASP (e.g., due to some mathematical functions not supported by the ASP solvers) but can be easily implemented in C++.

Designing agents that reason and act upon the world has always been one of the main objectives of the Artificial Intelligence community. While for planning in “simple” domains the agents can solely rely on facts about the world, in several contexts, e.g., economy, security, justice and politics, the mere knowledge of the world could be insufficient to reach a desired goal. In these scenarios, epistemic reasoning, i.e., reasoning about agents’ beliefs about themselves and about other agents’ beliefs, is essential to design winning strategies. This paper addresses the problem of reasoning in multi-agent epistemic settings exploiting declarative programming techniques. In particular, the paper presents an actual implementation of a multi-shot Answer Set Programming-based planner that can reason in multi-agent epistemic settings, called PLATO (ePistemic muLti-agent Answer seT programming sOlver). The ASP paradigm enables a concise and elegant design of the planner, w.r.t. other imperative implementations, facilitating the development of formal verification of correctness. The paper shows how the planner, exploiting an ad-hoc epistemic state representation and the efficiency of ASP solvers, has competitive performance results on benchmarks collected from the literature.

We introduce a novel logic-based system for reasoning over data streams, which relies on a framework enabling a tight, fine-tuned interaction between Apache Flink and the $${{\mathcal I}^2}$$ -DLV system. The architecture allows to take advantage from both the powerful distributed stream processing capabilities of Flink and the incremental reasoning capabilities of $${{\mathcal I}^2}$$ -DLV, based on overgrounding techniques. Besides the system architecture, we illustrate the supported input language and its modeling capabilities, and discuss the results of an experimental activity aimed at assessing the viability of the approach.

Weighted knowledge bases for description logics with typicality have been recently considered under a “concept-wise” multipreference semantics (in both the two-valued and fuzzy case), as the basis of a logical semantics of multilayer perceptrons (MLPs). In this paper we consider weighted conditional $\mathcal{ALC}$ knowledge bases with typicality in the finitely many-valued case, through three different semantic constructions. For the boolean fragment $\mathcal{LC}$ of $\mathcal{ALC}$ we exploit answer set programming and asprin for reasoning with the concept-wise multipreference entailment under a $\varphi$ -coherent semantics, suitable to characterize the stationary states of MLPs. As a proof of concept, we experiment the proposed approach for checking properties of trained MLPs.

Given a causal model of some domain and a particular story that has taken place in this domain, the problem of actual causation is deciding which of the possible causes for some effect actually caused it. One of the most influential approaches to this problem has been developed by Halpern and Pearl (Halpern, J. and Pearl, J. 2005. Causes and explanations: A structural-model approach. Part I: Causes. British Journal for the Philosophy of Science 56(4), 843–887) in the context of structural models. In this paper, I argue that this is actually not the best setting for studying this problem. As an alternative, I offer the probabilistic logic programming language of CP-logic. Unlike structural models, CP-logic incorporates the deviant/default distinction that is generally considered an important aspect of actual causation, and it has an explicitly dynamic semantics, which helps to formalize the stories that serve as input to an actual causation problem.

We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal an appealing formulation for capturing the well-founded semantics for higher-order logic programs.

The dlvhex system implements the hex-semantics, which integrates answer set programming (ASP) with arbitrary external sources. Since its first release ten years ago, significant advancements were achieved. Most importantly, the exploitation of properties of external sources led to efficiency improvements and flexibility enhancements of the language, and technical improvements on the system side increased user's convenience. In this paper, we present the current status of the system and point out the most important recent enhancements over early versions. While existing literature focuses on theoretical aspects and specific components, a bird's eye view of the overall system is missing. In order to promote the system for real-world applications, we further present applications which were already successfully realized on top of dlvhex.

Timed Concurrent Constraint Programming (tcc) is a declarative model for concurrency offering a logic for specifying reactive systems, i.e., systems that continuously interact with the environment. The universal tcc formalism (utcc) is an extension of tcc with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. In this paper we consider the denotational semantics for tcc, and extend it to a “collecting” semantics for utcc based on closure operators over sequences of constraints. Relying on this semantics, we formalize a general framework for data flow analyses of tcc and utcc programs by abstract interpretation techniques. The concrete and abstract semantics that we propose are compositional, thus allowing us to reduce the complexity of data flow analyses. We show that our method is sound and parametric with respect to the abstract domain. Thus, different analyses can be performed by instantiating the framework. We illustrate how it is possible to reuse abstract domains previously defined for logic programming to perform, for instance, a groundness analysis for tcc programs. We show the applicability of this analysis in the context of reactive systems. Furthermore, we also make use of the abstract semantics to exhibit a secrecy flaw in a security protocol. We also show how it is possible to make an analysis which may show that tcc programs are suspension-free. This can be useful for several purposes, such as for optimizing compilation or for debugging.

This paper presents a programming language which includes paradigms that are usually associated with declarative languages, such as sets, rules and search, into an imperative (functional) language. Although these paradigms are separately well known and are available under various programming environments, the originality of the CLAIRE language comes from the tight integration, which yields interesting run-time performances, and from the richness of this combination, which yields new ways in which to express complex algorithmic patterns with few elegant lines. To achieve the opposite goals of a high abstraction level (conciseness and readability) and run-time performance (CLAIRE is used as a C++ preprocessor), we have developed two kinds of compiler: first, a pattern pre-processor handles iterations over both concrete and abstract sets (data types and program fragments), in a completely user-extensible manner; secondly, an inference compiler transforms a set of logical rules into a set of functions (demons that are used through procedural attachment).

The goal of this paper is to provide a strong integration between constraint modelling and relational DBMSs. To this end we propose extensions of standard query languages such as relational algebra and SQL, by adding constraint modelling capabilities to them. In particular, we propose non-deterministic extensions of both languages, which are specially suited for combinatorial problems. Non-determinism is introduced by means of a guessing operator, which declares a set of relations to have an arbitrary extension. This new operator results in languages with higher expressive power, able to express all problems in the complexity class NP. Some syntactical restrictions which make data complexity polynomial are shown. The effectiveness of both extensions is demonstrated by means of several examples. The current implementation, written in Java using local search techniques, is described.

The Decision Model and Notation (DMN) is a recent Object Management Group standard for the elicitation and representation of decision models and for managing their interconnection with business processes. DMN builds on the notion of decision tables and their combination into more complex decision requirements graphs (DRGs), which bridge between business process models and decision logic models. DRGs may rely on additional, external business knowledge models, whose functioning is not part of the standard. In this work, we consider one of the most important types of business knowledge, namely, background knowledge that conceptually accounts for the structural aspects of the domain of interest, and propose decision knowledge bases (DKBs), which semantically combine DRGs modeled in DMN, and domain knowledge captured by means of first-order logic with datatypes. We provide a logic-based semantics for such an integration, and formalize different DMN reasoning tasks for DKBs. We then consider background knowledge formulated as a description logic (DL) ontology with datatypes, and show how the main verification tasks for DMN in this enriched setting can be formalized as standard DL reasoning services and actually carried out in ExpTime. We discuss the effectiveness of our framework on a case study in maritime security.

Anti-unification refers to the process of generalizing two (or more) goals into a single, more general, goal that captures some of the structure that is common to all initial goals. In general one is typically interested in computing what is often called a most specific generalization, that is a generalization that captures a maximal amount of shared structure. In this work we address the problem of anti-unification in CLP, where goals can be seen as unordered sets of atoms and/or constraints. We show that while the concept of a most specific generalization can easily be defined in this context, computing it becomes an NP-complete problem. We subsequently introduce a generalization algorithm that computes a well-defined abstraction whose computation can be bound to a polynomial execution time. Initial experiments show that even a naive implementation of our algorithm produces acceptable generalizations in an efficient way.

Building Information Modeling (BIM) produces three-dimensional object-oriented models of buildings combining the geometrical information with a wide range of properties about materials, products, safety, to name just a few. BIM is slowly but inevitably revolutionizing the architecture, engineering, and construction industry. Buildings need to be compliant with regulations about stability, safety, and environmental impact. Manual compliance checking is tedious and error-prone, and amending flaws discovered only at construction time causes huge additional costs and delays. Several tools can check BIM models for conformance with rules/guidelines. For example, Singapore’s CORENET e-Submission System checks fire safety. But since the current BIM exchange format only contains basic information about building objects, a separate, ad-hoc model pre-processing is required to determine, for example, evacuation routes. Moreover, they face difficulties in adapting existing built-in rules and/or adding new ones (to cater for building regulations, that can vary not only among countries but also among parts of the same city), if at all possible. We propose the use of logic-based executable formalisms (CLP and Constraint ASP) to couple BIM models with advanced knowledge representation and reasoning capabilities. Previous experience shows that such formalisms can be used to uniformly capture and reason with knowledge (including ambiguity) in a large variety of domains. Additionally, incorporating checking within design tools makes it possible to ensure that models are rule-compliant at every step. This also prevents erroneous designs from having to be (partially) redone, which is also costly and burdensome. To validate our proposal, we implemented a preliminary reasoner under CLP(Q/R) and ASP with constraints and evaluated it with several BIM models.

There is a growing need for abstractions in logic specification languages such as FO(·) and ASP. One technique to achieve these abstractions are templates (sometimes called macros). While the semantics of templates are virtually always described through a syntactical rewriting scheme, we present an alternative view on templates as second order definitions. To extend the existing definition construct of FO(·) to second order, we introduce a powerful compositional framework for defining logics by modular integration of logic constructs specified as pairs of one syntactical and one semantical inductive rule. We use the framework to build a logic of nested second order definitions suitable to express templates. We show that under suitable restrictions, the view of templates as macros is semantically correct and that adding them does not extend the descriptive complexity of the base logic, which is in line with results of existing approaches.

In recent years, answer set programming (ASP) has been extended to deal with multivalued predicates. The resulting formalismsallow for the modeling of continuous problems as elegantly as ASP allows for the modeling of discrete problems, by combining thestable model semantics underlying ASP with fuzzy logics. However, contrary to the case of classical ASP where manyefficient solvers have been constructed, to date there is no efficient fuzzy ASP solver. A well-knowntechnique for classical ASP consists of translating an ASP program P to a propositional theory whose models exactlycorrespond to the answer sets of P. In this paper, we show how this idea can be extended to fuzzy ASP, paving the wayto implement efficient fuzzy ASP solvers that can take advantage of existing fuzzy logic reasoners.

Using the notion of an elementary loop, Gebser and Schaub (2005. Proceedings of the Eighth International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'05), 53–65) refined the theorem on loop formulas attributable to Lin and Zhao (2004) by considering loop formulas of elementary loops only. In this paper, we reformulate the definition of an elementary loop, extend it to disjunctive programs, and study several properties of elementary loops, including how maximal elementary loops are related to minimal unfounded sets. The results provide useful insights into the stable model semantics in terms of elementary loops. For a nondisjunctive program, using a graph-theoretic characterization of an elementary loop, we show that the problem of recognizing an elementary loop is tractable. On the other hand, we also show that the corresponding problem is coNP-complete for a disjunctive program. Based on the notion of an elementary loop, we present the class of Head-Elementary-loop-Free (HEF) programs, which strictly generalizes the class of Head-Cycle-Free (HCF) programs attributable to Ben-Eliyahu and Dechter (1994. Annals of Mathematics and Artificial Intelligence 12, 53–87). Like an HCF program, an HEF program can be turned into an equivalent nondisjunctive program in polynomial time by shifting head atoms into the body.

Tabling is probably the most widely studied extension of Prolog. But despite its importance and practicality, tabling is not implemented by most Prolog systems. Existing approaches require substantial changes to the Prolog engine, which is an investment out of reach of most systems. To enable more widespread adoption, we present a new implementation of tabling in under 600 lines of Prolog code. Our lightweight approach relies on delimited control and provides reasonable performance.

In Probabilistic Logic Programming (PLP) the most commonly studied inference task is to compute the marginal probability of a query given a program. In this paper, we consider two other important tasks in the PLP setting: the Maximum-A-Posteriori (MAP) inference task, which determines the most likely values for a subset of the random variables given evidence on other variables, and the Most Probable Explanation (MPE) task, the instance of MAP where the query variables are the complement of the evidence variables. We present a novel algorithm, included in the PITA reasoner, which tackles these tasks by representing each problem as a Binary Decision Diagram and applying a dynamic programming procedure on it. We compare our algorithm with the version of ProbLog that admits annotated disjunctions and can perform MAP and MPE inference. Experiments on several synthetic datasets show that PITA outperforms ProbLog in many cases.