Modern functional logic programming (FLP) languages use non-terminating and non-confluent constructor systems (CSs) as programs in order to define non-strict and non-deterministic functions. Two semantic alternatives have been usually considered for parameter passing with this kind of functions: call-time choice and run-time choice. While the former is the standard choice of modern FLP languages, the latter lacks some basic properties – mainly compositionality – that have prevented its use in practical FLP systems. Traditionally it has been considered that call-time choice induces a singular denotational semantics, while run-time choice induces a plural semantics. We have discovered that this latter identification is wrong when pattern matching is involved, and thus in this paper we propose two novel compositional plural semantics for CSs that are different from run-time choice.

We investigate the basic properties of our plural semantics – compositionality, polarity, and monotonicity for substitutions, and a restricted form of the bubbling property for CSs – and the relation between them and to previous proposals, concluding that these semantics form a hierarchy in the sense of set inclusion of the set of values computed by them. Besides, we have identified a class of programs characterized by a simple syntactic criterion for which the proposed plural semantics behave the same, and a program transformation that can be used to simulate one of the proposed plural semantics by term rewriting. At the practical level, we study how to use the new expressive capabilities of these semantics for improving the declarative flavor of programs. As call-time choice is the standard semantics for FLP, it still remains the best option for many common programming patterns. Therefore, we propose a language that combines call-time choice and our plural semantics, which we have implemented in the Maude system. The resulting interpreter is then employed to develop and test several significant examples showing the capabilities of the combined semantics.

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.

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.

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.

CLP(H) is an instantiation of the general constraint logic programming scheme with the constraint domain of hedges. Hedges are finite sequences of unranked terms, built over variadic function symbols and three kinds of variables: for terms, for hedges, and for function symbols. Constraints involve equations between unranked terms and atoms for regular hedge language membership. We study algebraic semantics of CLP(H) programs, define a sound, terminating, and incomplete constraint solver, investigate two fragments of constraints for which the solver returns a complete set of solutions, and describe classes of programs that generate such constraints.

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.

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.

A classical result in descriptive complexity theory states that Datalog expresses exactly the class of polynomially computable queries on ordered databases (Papadimitriou 1985; Grädel 1992; Vardi 1982; Immerman 1986; Leivant 1989). In this paper we extend this result to the case of higher-order Datalog. In particular, we demonstrate that on ordered databases, for all k ≥ 2, k-order Datalog captures (k − 1)-EXPTIME. This result suggests that higher-order extensions of Datalog possess superior expressive power and they are worthwhile of further investigation both in theory and in practice.

The input language of the answer set solver clingo is based on the definition of a stable model proposed by Paolo Ferraris. The semantics of the ASP-Core language, developed by the ASP Standardization Working Group, uses the approach to stable models due to Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. The two languages are based on different versions of the stable model semantics, and the ASP-Core document requires, “for the sake of an uncontroversial semantics,” that programs avoid the use of recursion through aggregates. In this paper we prove that the absence of recursion through aggregates does indeed guarantee the equivalence between the two versions of the stable model semantics, and show how that requirement can be relaxed without violating the equivalence property.

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.

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.

We describe an application of Answer Set Programming to the understanding of narratives about stereotypical activities, demonstrated via question answering. Substantial work in this direction was done by Erik Mueller, who modeled stereotypical activities as scripts. His systems were able to understand a good number of narratives, but could not process texts describing exceptional scenarios. We propose addressing this problem by using a theory of intentions developed by Blount, Gelfond, and Balduccini. We present a methodology in which we substitute scripts by activities (i.e., hierarchical plans associated with goals) and employ the concept of an intentional agent to reason about both normal and exceptional scenarios. We exemplify the application of this methodology by answering questions about a number of restaurant stories. This paper is under consideration for acceptance in TPLP.

The widespread availability of large data-sets poses both an opportunity and a challenge to logic programming. A first approach is to couple a relational database with logic programming, say, a Prolog system with MySQL. While this approach does pay off in cases where the data cannot reside in main memory, it is known to introduce substantial overheads. Ideally, we would like the Prolog system to deal with large data-sets in an efficient way both in terms of memory and of processing time. Just In Time Indexing (JITI) was mainly motivated by this challenge, and can work quite well in many application.

Exo-compilation, designed to deal with large tables, is a next step that achieves very interesting results, reducing the memory footprint over two thirds. We show that combining exo-compilation with Just In Time Indexing can have significant advantages both in terms of memory usage and in terms of execution time.

An alternative path that is relevant for many applications is User-Defined Indexing (UDI). This allows the use of specialized indexing for specific applications, say the spatial indexing crucial to any spatial system. The UDI sees indexing as pluggable modules, and can naturally be combined with Exo-compilation. We do so by using UDI with exo-data, and incorporating ideas from the UDI into high-performance indexers for specific tasks.

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.

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.

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.

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