ABSTRACT. The success of SAT solving, Answer Set Programming, and Model Checking has changed our view of computational complexity and (un)decidability. Program committees are increasingly discussing the value of theoretical and empirical complexity evaluations. What is the intellectual value of a completeness result? Which standards do we apply to reproducibility of experiments? What is the role of competitions? What are the minimal requirements for an experimental proof of concept?

ABSTRACT. We have designed a new logic programming language called LM (Linear Meld) for programming graph-based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where logical facts can be consumed. Because LM integrates both classical and linear logic, LM tends to be more expressive than other logic programming languages. LM programs are naturally concurrent because facts are partitioned by nodes of a graph data structure. Computation is performed at the node level while communication happens between connected nodes. In this paper, we present the syntax and operational semantics of our language and illustrate its use through a number of examples.

ABSTRACT. Lifted inference has been proposed for various probabilistic logical frameworks in order to compute the probability of queries in a time that is polynomial in the size of the domains of the logical variables rather than exponential. Even if various authors have underlined its importance for probabilistic logic programming (PLP), lifted inference has been applied up to now only to relational languages outside of logic programming. In this paper we adapt Generalized Counting First Order Variable Elimination (GC-FOVE) to the problem of computing the probability of queries to probabilistic logic programs under the distribution semantics. In particular, we extend the Prolog Factor Language (PFL) to include two new types of factors that are needed for representing ProbLog programs. These factors take into account the existing causal independence relationships among some of the random variables and are managed by the extension to variable elimination proposed by Zhang and Poole for dealing with convergent variables and heterogeneous factors. Two new operators are added to GC-FOVE for treating heterogeneous factors. The resulting algorithm, called LP$^2$ for Lifted Probabilistic Logic Programming, has been implemented by modifying the PFL implementation of GC-FOVE and tested on three benchmarks for lifted inference. The comparison with PITA and ProbLog2 shows the potential of the approach.

ABSTRACT. Extensional higher-order logic programming has been introduced as a generalization of classical logic programming. An important characteristic of this paradigm is that it preserves all the well-known properties of traditional logic programming. In this paper we consider the semantics of negation in the context of the new paradigm. Using some recent results from non-monotonic fixed-point theory, we demonstrate that every higher-order logic program with negation has a unique minimum infinite-valued model. In this way we obtain the first purely model-theoretic semantics for negation in extensional higher-order logic programming. Using our approach, we resolve an old paradox that was introduced by W. W. Wadge in order to demonstrate the semantic difficulties of higher-order logic programming.

ABSTRACT. 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 subset 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.

ABSTRACT. Domain-specific languages (DSLs) are routinely created to simplify difficult or specialized programming tasks. They expose useful abstractions and design patterns in the form of language constructs, provide static semantics to eagerly detect misuse of these constructs, and dynamic semantics to completely define how language constructs interact. However, implementing and composing DSLs is a non-trivial task, and there is a lack of tools and techniques.

We address this problem by presenting a complete module system over LP for DSL construction, reuse, and composition. LP is already useful for DSL design, because it supports executable language specifications using notations familiar to language designers. We extend LP with a module system that is simple (with a few concepts), succinct (for key DSL specification scenarios), and composable (on the level of languages, compilers, and programs). These design choices reflect our use of LP for industrial DSL design. Our module system has been implemented in the FORMULA language, and was used to build key Windows 8 device drivers via DSLs. Though we present our module system as it actually appear in our FORMULA language, our emphasis is on concepts adaptable to other LP languages.

ABSTRACT. When developing a (web) interface for a deductive database, functionality required by the client is provided by means of HTTP handlers that wrap the logical data access predicates. These handlers are responsible for converting between client and server data representations and typically include options for paginating results. Designing the web accessible API is difficult because it is hard to predict the exact requirements of clients. Pengines changes this picture. The client provides a Prolog program that selects the required data by accessing the logical API of the server. The pengine infrastructure provides general mechanisms for converting Prolog data and handling Prolog non-determinism. The Pengines library is small (2000 lines Prolog, 100 lines JavaScript). It greatly simplifies defining an AJAX based client for a Prolog program, but also provides non-deterministic RPC between Prolog processes as well as interaction with Prolog engines similar to Paul Tarau's engines. Pengines are available as a standard package for SWI-Prolog~7.

ABSTRACT. Resolution-based Knowledge Representation and Reasoning (KRR) systems, such as Flora-2, Silk or Ergo, can scale to tens or hundreds of millions of facts, while supporting reasoning that includes Hilog, inheritance, defeasibility theories, and equality theories. These systems handle the termination and complexity issues that arise from the use of these features by a heavy use of tabling. In fact, such systems table by default all rules defined by users, unless they are simple facts.

Performing dynamic updates within such systems is nearly impossible unless the tables themselves can be made to react to changes. Incremental tabling as implemented in XSB~\cite{Saha06} partially addressed this problem, but the implementation was limited in scope and not always easy to use. In this paper, we describe {\em automatic incremental tabling} which at the semantic level supports updates in the 3-valued well-founded semantics, while guaranteeing full consistency of all tabled queries. Automatic Incremental Tabling also has significant performance improvements over previous implementations, including lazy incremental tabling, and control over the dependency structures used to determine how tables are updated. %Benchmarks indicate that \automatic incremental tabling has major %performance improvements over previous versions of incremental %tabling.

ABSTRACT. Tabling is a commonly used technique in logic programming for avoiding cyclic behavior of logic programs and enabling more declarative program definitions. Furthermore, tabling often results in improved computation performance. Rational term are terms with one or more infinite sub-terms but with a finite representation. Rational terms can be generated in Prolog by omitting the occurs check when unifying two terms. Applications of rational terms include definite clause grammars, constraint handling systems, and coinduction. In this paper we report our extension of Yap's Prolog tabling mechanism to support rational terms. We describe the internal representation of rational terms within the table space and prove its correctness. We use this extension to implement a novel approach to coinduction with the use of tabling. We present the similarities with current coinductive transformations and describe the implementation. In addition, we address some limitations of rational terms support by Prolog compilers and describe an approach to ensure a canonical representation for rational terms.