We study algorithms for computing stable models of logic programs and derive estimates on their worst-case performance that are asymptotically better than the trivial bound of $O(m 2^n)$, where $m$ is the size of an input program and $n$ is the number of its atoms. For instance, for programs whose clauses consist of at most two literals (counting the head) we design an algorithm to compute stable models that works in time $O(m\times 1.44225^n)$. We present similar results for several broader classes of programs. Finally, we study the applicability of the techniques developed in the paper to the analysis of the performance of smodels.

Most cities in Germany regularly publish a booklet called the Mietspiegel. It basically contains a verbal description of an expert system. It allows the calculation of the estimated fair rent for a flat. By hand, one may need a weekend to do this task. With our computerized version, the Munich Rent Advisor, the user just fills in a form in a few minutes, and the rent is calculated immediately. We also extended the functionality and applicability of the Mietspiegel so that the user need not answer all questions on the form. The key to computing with partial information using high-level programming was to use constraint logic programming. We rely on the Internet, and more specifically the World Wide Web, to provide this service to a broad user group, the citizens of Munich and the people who are planning to move to Munich. To process the answers from the questionnaire and return its result, we wrote a small simple stable special-purpose web server directly in ECLiPSe. More than 10,000 people have used our service in the last three years. This article describes the experiences in implementing and using the Munich Rent Advisor. Our results suggest that logic programming with constraints can be an important ingredient in intelligent internet systems.

Weight constraint and aggregate programs are among the most widely used logic programs with constraints. In this paper, we relate the semantics of these two classes of programs, namely, the stable model semantics for weight constraint programs and the answer set semantics based on conditional satisfaction for aggregate programs. Both classes of programs are instances of logic programs with constraints, and in particular, the answer set semantics for aggregate programs can be applied to weight constraint programs. We show that the two semantics are closely related. First, we show that for a broad class of weight constraint programs, called strongly satisfiable programs, the two semantics coincide. When they disagree, a stable model admitted by the stable model semantics may be circularly justified. We show that the gap between the two semantics can be closed by transforming a weight constraint program to a strongly satisfiable one so that no circular models may be generated under the current implementation of the stable model semantics. We further demonstrate the close relationship between the two semantics by formulating a transformation from weight constraint programs to logic programs with nested expressions, which preserves the answer set semantics. Our study on the semantics leads to an investigation of a methodological issue, namely, the possibility of compact representation of aggregate programs by weight constraint programs. We show that almost all standard aggregates can be encoded by weight constraints compactly. This makes it possible to compute the answer sets of aggregate programs using the answer set programming solvers for weight constraint programs. This approach is compared experimentally with the ones where aggregates are handled more explicitly, which show that the weight constraint encoding of aggregates enables a competitive approach to answer set computation for aggregate programs.

ISO Prolog provides catch and throw to realize the control flow of exception handling. This pearl demonstrates that catch and throw are inconspicuously amenable to the implementation of backjumping. In fact, they have precisely the semantics required: rewinding the search to a specific point and carrying of a preserved term to that point. The utility of these properties is demonstrated through an implementation of graph coloring with backjumping and a backjumping SAT solver that applies conflict-driven clause learning.

Thom Frühwirth presented a short, elegant, and efficient Prolog program for the n queens problem. However, the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way and provides proofs of its correctness and completeness. The specification and the proofs are declarative, that is they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program’s semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations. Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program.

Cooperation among constraint solvers is difficult because different solving paradigms have different theoretical foundations. Recent works have shown that abstract interpretation can provide a unifying theory for various constraint solvers. In particular, it relies on abstract domains which capture constraint languages as ordered structures. The key insight of this paper is viewing cooperation schemes as abstract domains combinations. We propose a modular framework in which solvers and cooperation schemes can be seamlessly added and combined. This differs from existing approaches such as SMT where the cooperation scheme is usually fixed (e.g., Nelson-Oppen). We contribute to two new cooperation schemes: (i) interval propagators completion that allows abstract domains to exchange bound constraints, and (ii) delayed product which exchanges over-approximations of constraints between two abstract domains. Moreover, the delayed product is based on delayed goal of logic programming, and it shows that abstract domains can also capture control aspects of constraint solving. Finally, to achieve modularity, we propose the shared product to combine abstract domains and cooperation schemes. Our approach has been fully implemented, and we provide various examples on the flexible job shop scheduling problem.

This paper investigates the relationship between the Logical Algorithms (LA) language of Ganzinger and McAllester and Constraint Handling Rules (CHR). We present a translation schema from LA to CHRrp: CHR with rule priorities, and show that the meta-complexity theorem for LA can be applied to a subset of CHRrp via inverse translation. Inspired by the high-level implementation proposal for Logical Algorithm by Ganzinger and McAllester and based on a new scheduling algorithm, we propose an alternative implementation for CHRrp that gives strong complexity guarantees and results in a new and accurate meta-complexity theorem for CHRrp. It is furthermore shown that the translation from Logical Algorithms to CHRrp combined with the new CHRrp implementation satisfies the required complexity for the Logical Algorithms meta-complexity result to hold.

Time is a crucial factor in modelling dynamic behaviours of intelligent agents: activities have a determined temporal duration in a real-world environment, and previous actions influence agents’ behaviour. In this paper, we propose a language for modelling concurrent interaction between agents that also allows the specification of temporal intervals in which particular actions occur. Such a language exploits a timed version of Abstract Argumentation Frameworks to realise a shared memory used by the agents to communicate and reason on the acceptability of their beliefs with respect to a given time interval. An interleaving model on a single processor is used for basic computation steps, with maximum parallelism for time elapsing. Following this approach, only one of the enabled agents is executed at each moment. To demonstrate the capabilities of the language, we also show how it can be used to model interactions such as debates and dialogue games taking place between intelligent agents. Lastly, we present an implementation of the language that can be accessed via a web interface.

A sufficient and necessary condition is given under which least Herbrand models exactly characterize the answers of definite clause programs.

Our broader goal is to automatically translate English sentences into formulas in appropriate knowledge representation languages as a step towards understanding and thus answering questions with respect to English text. Our focus in this paper is on the language of Answer Set Programming (ASP). Our approach to translate sentences to ASP rules is inspired by Montague's use of lambda calculus formulas as meaning of words and phrases. With ASP as the target language the meaning of words and phrases are ASP-lambda formulas. In an earlier work we illustrated our approach by manually developing a dictionary of words and their ASP-lambda formulas. However such an approach is not scalable. In this paper our focus is on two algorithms that allow one to construct ASP-lambda formulas in an inverse manner. In particular the two algorithms take as input two lambda-calculus expressions G and H and compute a lambda-calculus expression F such that F with input as G, denoted by F@G, is equal to H; and similarly G@F = H. We present correctness and complexity results about these algorithms. To do that we develop the notion of typed ASP-lambda calculus theories and their orders and use it in developing the completeness results.

Tau Prolog is a client-side Prolog interpreter fully implemented in JavaScript, which aims at implementing the ISO Prolog Standard. Tau Prolog has been developed to be used with either Node.js or a browser seamlessly, and therefore, it has been developed following a non-blocking, callback-based approach to avoid blocking web browsers. Taking the best from JavaScript and Prolog, Tau Prolog allows the programmer to handle browser events and manipulate the Document Object Model (DOM) of a web using Prolog predicates. In this paper we describe the architecture of Tau Prolog and its main packages for interacting with the Web, and we present its programming environment.

Nowadays, clusters of multicores are becoming the norm and, although, many or-parallel Prolog systems have been developed in the past, to the best of our knowledge, none of them was specially designed to explore the combination of shared and distributed memory architectures. In recent work, we have proposed a novel computational model specially designed for such combination which introduces a layered model with two scheduling levels, one for workers sharing memory resources, which we named a team of workers, and another for teams of workers (not sharing memory resources). In this work, we present a first implementation of such model and for that we revive and extend the YapOr system to exploit or-parallelism between teams of workers. We also propose a new set of built-in predicates that constitute the syntax to interact with an or-parallel engine in our platform. Experimental results show that our implementation is able to increase speedups as we increase the number of workers per team, thus taking advantage of the maximum number of cores in a machine, and to increase speedups as we increase the number of teams, thus taking advantage of adding more computer nodes to a cluster.

The runtime system of dynamic languages such as Prolog or Lisp and their derivatives contain a symbol table, in Prolog often called the atom table. A simple dynamically resizing hash-table used to be an adequate way to implement this table. As Prolog becomes fashionable for 24 × 7 server processes we need to deal with atom garbage collection and concurrent access to the atom table. Classical lock-based implementations to ensure consistency of the atom table scale poorly and a stop-the-world approach to implement atom garbage collection quickly becomes a bottle-neck, making Prolog unsuitable for soft real-time applications. In this article we describe a novel implementation for the atom table using lock-free techniques where the atom-table remains accessible even during atom garbage collection. Relying only on CAS (Compare And Swap) and not on external libraries, the implementation is straightforward and portable.

The infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas.

Control flow compilation is a hybrid between classical WAM compilation and meta-call, limited to the compilation of non-recursive clause bodies. This approach is used successfully for the execution of dynamically generated queries in an inductive logic programming setting (ILP). Control flow compilation reduces compilation times up to an order of magnitude, without slowing down execution. A lazy variant of control flow compilation is also presented. By compiling code by need, it removes the overhead of compiling unreached code (a frequent phenomenon in practical ILP settings), and thus reduces the size of the compiled code. Both dynamic compilation approaches have been implemented and were combined with query packs, an efficient ILP execution mechanism. It turns out that locality of data and code is important for performance. The experiments reported in the paper show that lazy control flow compilation is superior in both artificial and real life settings.

Answer Set Programming (ASP) is a well-established formalism for logic programming. Problem solving in ASP requires to write an ASP program whose answers sets correspond to solutions. Albeit the non-existence of answer sets for some ASP programs can be considered as a modeling feature, it turns out to be a weakness in many other cases, and especially for query answering. Paracoherent answer set semantics extend the classical semantics of ASP to draw meaningful conclusions also from incoherent programs, with the result of increasing the range of applications of ASP. State of the art implementations of paracoherent ASP adopt the semi-equilibrium semantics, but cannot be lifted straightforwardly to compute efficiently the (better) split semi-equilibrium semantics that discards undesirable semi-equilibrium models. In this paper an efficient evaluation technique for computing a split semi-equilibrium model is presented. An experiment on hard benchmarks shows that better paracoherent answer sets can be computed consuming less computational resources than existing methods.

Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the environment, while satisfying certain conditions that are formally specified. Such problems are found in, for example, engineering, law or economics. We study this class of problems in a context where some of the relevant information about the environment is not known by the user at the start of the search. During the search, the user may consider tentative solutions that make implicit hypotheses about these unknowns. To ensure that the solution is appropriate, these hypotheses must be verified by observing the environment. Furthermore, we assume that, in addition to knowledge of what constitutes a solution, knowledge of general laws of the environment is also present. We formally define partial solutions with enough verified facts to guarantee the existence of complete and appropriate solutions. Additionally, we propose an interactive system to assist the user in their search by determining (1) which hypotheses implicit in a tentative solution must be verified in the environment, and (2) which observations can bring useful information for the search. We present an efficient method to over-approximate the set of relevant information, and evaluate our implementation.