We argue that turning a logic program into a set of completed definitions can be sometimes thought of as the “reverse engineering” process of generating a set of conditions that could serve as a specification for it. Accordingly, it may be useful to define completion for a large class of Answer Set Programming (ASP) programs and to automate the process of generating and simplifying completion formulas. Examining the output produced by this kind of software may help programmers to see more clearly what their program does, and to what degree its behavior conforms with their expectations. As a step toward this goal, we propose here a definition of program completion for a large class of programs in the input language of the ASP grounder gringo, and study its properties.

We investigate the problem of cost-optimal planning in ASP. Current ASP planners can be trivially extended to a cost-optimal one by adding weak constraints, but only for a given makespan (number of steps). It is desirable to have a planner that guarantees global optimality. In this paper, we present two approaches to addressing this problem. First, we show how to engineer a cost-optimal planner composed of two ASP programs running in parallel. Using lessons learned from this, we then develop an entirely new approach to cost-optimal planning, stepless planning, which is completely free of makespan. Experiments to compare the two approaches with the only known cost-optimal planner in SAT reveal good potentials for stepless planning in ASP.

A Hidden Markov Model (HMM) is a common statistical model which is widely used for analysis of biological sequence data and other sequential phenomena. In the present paper we show how HMMs can be extended with side-constraints and present constraint solving techniques for efficient inference. Defining HMMs with side-constraints in Constraint Logic Programming has advantages in terms of more compact expression and pruning opportunities during inference. We present a PRISM-based framework for extending HMMs with side-constraints and show how well-known constraints such as cardinality and all_different are integrated. We experimentally validate our approach on the biologically motivated problem of global pairwise alignment.

Some normal logic programs under the answer set (or stable model) semantics lack the appealing property of ‘cautious monotonicity.’ That is, augmenting a program with one of its consequences may cause it to lose another of its consequences. The syntactic condition of ‘order-consistency’ was shown by Fages to guarantee existence of an answer set. This note establishes that order-consistent programs are not only consistent, but cautiously monotonic. From this it follows that they are also ‘cumulative’. That is, augmenting an order-consistent program with some of its consequences does not alter its consequences. In fact, as we show, its answer sets remain unchanged.

This paper introduces a framework for assisting policy authors in refining and improving their policies. In particular, we focus on authorization and obligation policies that can be encoded in Gelfond and Lobo’s $\mathscr{AOPL}$ language for policy specification. We propose a framework that detects the statements that make a policy inconsistent, underspecified, or ambiguous with respect to an action being executed in a given state. We also give attention to issues that arise at the intersection of authorization and obligation policies, for instance when the policy requires an unauthorized action to be executed. The framework is encoded in Answer Set Programming.

Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many answer set programs. We also introduce conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. We show how the notion of a conservative extension can be used to justify the common projection rewriting.

This paper explores the integration of hypothetical reasoning into an efficient implementation of the fuzzy logic language Bousi∼Prolog. To this end, we first analyse what would be expected from a logic inference system, equipped with what is called embedded implication, to model solving goals with respect to assumptions. We start with a propositional system and incrementally build more complex systems and implementations to satisfy the requirements imposed by a system like Bousi∼Prolog. Finally, we propose an inference system, operational semantics and the translation function to generate efficient Prolog programmes from Bousi∼Prolog programmes.

On top of a neural network-based dependency parser and a graph-based natural language processing module, we design a Prolog-based dialog engine that explores interactively a ranked fact database extracted from a text document. We reorganize dependency graphs to focus on the most relevant content elements of a sentence and integrate sentence identifiers as graph nodes. Additionally, after ranking the graph, we take advantage of the implicit semantic information that dependency links and WordNet bring in the form of subject–verb–object, “is-a” and “part-of” relations. Working on the Prolog facts and their inferred consequences, the dialog engine specializes the text graph with respect to a query and reveals interactively the document’s most relevant content elements. The open-source code of the integrated system is available at https://github.com/ptarau/DeepRank.

The Winograd Schema Challenge (WSC) is a natural language understanding task proposed as an alternative to the Turing test in 2011. In this work we attempt to solve WSC problems by reasoning with additional knowledge. By using an approach built on top of graph-subgraph isomorphism encoded using Answer Set Programming (ASP) we were able to handle 240 out of 291 WSC problems. The ASP encoding allows us to add additional constraints in an elaboration tolerant manner. In the process we present a graph based representation of WSC problems as well as relevant commonsense knowledge.

First-order resolution has been used for type inference for many years, including in Hindley-Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method.

The 31st edition of the International Conference of Logic Programming (ICLP 2015) took place in Cork, Ireland, from 31 August 2015 to 4 September 2015, co-located with the 21st International Conference on Principles and Practice of Constraint Programming (CP 2015) and part of George Boole 200, a celebration of the life and work of George Boole who was born in 1815 and worked at the University College of Cork.

The semantics of logic programs was originally described in terms of two-valued logic. Soon, however, it was realised that three-valued logic had some natural advantages, as it provides distinct values not only for truth and falsehood but also for “undefined”. The three-valued semantics proposed by Fitting (Fitting, M. 1985. A Kripke–Kleene semantics for logic programs. Journal of Logic Programming 2, 4, 295–312) and Kunen (Kunen, K. 1987. Negation in logic programming. Journal of Logic Programming 4, 4, 289–308) are closely related to what is computed by a logic program, the third truth value being associated with non-termination. A different three-valued semantics, proposed by Naish, shared much with those of Fitting and Kunen but incorporated allowances for programmer intent, the third truth value being associated with underspecification. Naish used an (apparently) novel “arrow” operator to relate the intended meaning of left and right sides of predicate definitions. In this paper we suggest that the additional truth values of Fitting/Kunen and Naish are best viewed as duals. We use Belnap's four-valued logic (Belnap, N. D. 1977. A useful four-valued logic. In Modern Uses of Multiple-Valued Logic, J. M. Dunn and G. Epstein, Eds. D. Reidel, Dordrecht, Netherlands, 8–37), also used elsewhere by Fitting, to unify the two three-valued approaches. The truth values are arranged in a bilattice, which supports the classical ordering on truth values as well as the “information ordering”. We note that the “arrow” operator of Naish (and our four-valued extension) is essentially the information ordering, whereas the classical arrow denotes the truth ordering. This allows us to shed new light on many aspects of logic programming, including program analysis, type and mode systems, declarative debugging and the relationships between specifications and programs, and successive execution states of a program.

Description logics (DLs) are well-known knowledge representation formalisms focused on the representation of terminological knowledge. Due to their first-order semantics, these languages (in their classical form) are not suitable for representing and handling uncertainty. A probabilistic extension of a light-weight DL was recently proposed for dealing with certain knowledge occurring in uncertain contexts. In this paper, we continue that line of research by introducing the Bayesian extension of the propositionally closed DL . We present a tableau-based procedure for deciding consistency and adapt it to solve other probabilistic, contextual, and general inferences in this logic. We also show that all these problems remain ExpTime-complete, the same as reasoning in the underlying classical .

Weighted logic programming, a generalization of bottom-up logic programming, is a well-suited framework for specifying dynamic programming algorithms. In this setting, proofs correspond to the algorithm's output space, such as a path through a graph or a grammatical derivation, and are given a real-valued score (often interpreted as a probability) that depends on the real weights of the base axioms used in the proof. The desired output is a function over all possible proofs, such as a sum of scores or an optimal score. We describe the product transformation, which can merge two weighted logic programs into a new one. The resulting program optimizes a product of proof scores from the original programs, constituting a scoring function known in machine learning as a “product of experts.” Through the addition of intuitive constraining side conditions, we show that several important dynamic programming algorithms can be derived by applying product to weighted logic programs corresponding to simpler weighted logic programs. In addition, we show how the computation of Kullback–Leibler divergence, an information-theoretic measure, can be interpreted using product.

Concurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude’s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.

The refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. In this paper we extend and generalise earlier work on contextual refinement. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program, which typically includes information about the values of the free variables. This paper also extends and generalises module refinement. A module is a collection of procedures that operate on a common data type; module refinement between a specification module A and an implementation module C allows calls to the procedures of A to be systematically replaced with calls to the corresponding procedures of C. Based on the conditions for module refinement, we present a method for calculating an implementation module from a specification module. Both contextual and module refinement within the refinement calculus have been generalised from earlier work and the results are presented in a unified framework.

Pointer analysis is a fundamental static program analysis for computing the set of objects that an expression can refer to. Decades of research has gone into developing methods of varying precision and efficiency for pointer analysis for programs that use different language features, but determining precisely how efficient a particular method is has been a challenge in itself.

For programs that use different language features, we consider methods for pointer analysis using Datalog and extensions to Datalog. When the rules are in Datalog, we present the calculation of precise time complexities from the rules using a new algorithm for decomposing rules for obtaining the best complexities. When extensions such as function symbols and universal quantification are used, we describe algorithms for efficiently implementing the extensions and the complexities of the algorithms.

Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which represents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and sometimes the needed fragment is quite huge.

In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpretation techniques) does not require to build any model at all. Our results guarantee correctness but, as usual when using an abstract semantics, completeness is lost.

Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is ΣP 2-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely dlv, gnt, cmodels, clasp and wasp. In this paper, we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers dlv, gnt, and cmodels. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers.

Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this article, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking.