Abstract We provide an approach to formally analyze the computational behavior of coroutines in logic programs and to compile these computations into new programs, not requiring any support for coroutines. The problem was already studied near to 30 years ago, in an analysis and transformation technique called compiling control. However, this technique had a strong ad hoc flavor: the completeness of the analysis was not well understood and its symbolic evaluation was also rather ad hoc. We show how abstract conjunctive partial deduction, introduced by Leuschel in 2004, provides an appropriate setting to redefine compiling control. We define an abstract domain and all abstract operations required by abstract conjunctive partial deduction. We prove that these concepts satisfy all the correctness conditions imposed by the framework and therefore inherit its main correctness theorem. We also show that there exist more complex coroutining examples which do not fit within abstract conjunctive partial deduction and we propose some further extensions to include them.

Abstract Riveret et al. have proposed a framework for probabilistic legal reasoning. Their goal is to determine the chance of winning a court case, given the probabilities of the judge accepting certain claimed facts and legal rules. In this paper we tackle the same problem by defining and implementing a new formalism, called probabilistic argumentation logic, which can be seen as a probabilistic generalization of Nute's defeasible logic. Not only does this provide an automation of the — only hand-performed — computations in Riveret et al, it also provides a solution to one of their open problems: a method to determine the initial probabilities from a given body of precedents.

Abstract Our goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

Abstract In the past years, analyzers have been introduced to detect classes of non-terminating queries for definite logic programs. Although these non-termination analyzers have shown to be rather precise, their applicability on real-life Prolog programs is limited because most Prolog programs use non-logical features. As a first step towards the analysis of Prolog programs, this paper presents a non-termination condition for Logic Programs containing integer arithmetics. The analyzer is based on our non-termination analyzer presented at International Logic Programming Conference (ICLP) 2009. The analysis starts from a class of queries and infers a subclass of non-terminating ones. In first phase, we ignore the outcome (success or failure) of the arithmetic operations, assuming success of all arithmetic calls. In second phase, we characterize successful arithmetic calls as a constraint problem, the solution of which determines the non-terminating queries.

Abstract We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of a logic program in case that neither a termination nor a non-termination proof is applicable. We establish a necessary and sufficient characterization of infinite (generalized) SLDNF-derivations with arbitrary (concrete or moded) queries, and develop an algorithm that predicts termination of general logic programs with arbitrary nonfloundering queries. We have implemented a termination prediction tool and obtained quite satisfactory experimental results. Except for five programs which break the experiment time limit, our prediction is 100% correct for all 296 benchmark programs of the Termination Competition 2007, of which 18 programs cannot be proved by any of the existing state-of-the-art analyzers like AProVE07, NTI, Polytool, and TALP.

The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis for a broad class of practical meta-interpreters, including negation and performing different tasks during the execution. It is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs. The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of those implies termination of the other one, i.e. the meta-interpreter preserves termination. Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.

We present a new approach to termination analysis of numerical computations in logic programs. Traditional approaches fail to analyse them due to non well-foundedness of the integers. We present a technique that allows overcoming these difficulties. Our approach is based on transforming a program in a way that allows integrating and extending techniques originally developed for analysis of numerical computations in the framework of query-mapping pairs with the well-known framework of acceptability. Such an integration not only contributes to the understanding of termination behaviour of numerical computations, but also allows us to perform a correct analysis of such computations automatically, by extending previous work on a constraint-based approach to termination. Finally, we discuss possible extensions of the technique, including incorporating general term orderings.

Tabled evaluation is receiving increasing attention in the logic programming community. It avoids many of the shortcomings of SLD execution and provides a more flexible and often considerably more efficient execution mechanism for logic programs. In particular, tabled execution terminates more often than execution based on SLD-resolution. In this article, we introduce two notions of universal termination of logic programming with tabling: quasi-termination and (the stronger notion of) LG-termination. We present sufficient conditions for these two notions of termination, namely quasi-acceptability and LG-acceptability, and we show that these conditions are also necessary in case the selection of tabled predicates meets certain natural criteria. Starting from these conditions, we develop modular termination proofs, i.e., proofs capable of combining termination proofs of separate programs to obtain termination proofs of combined programs. Finally, in the presence of mode information, we state sufficient conditions which form the basis for automatically proving termination in a constraint-based way.

Current norm-based automatic termination analysis techniques for logic programs can be split up into different components: inference of mode or type information, derivation of models, generation of well-founded orders, and verification of the termination conditions themselves. Although providing high-precision results, these techniques suffer from an efficiency point of view, as several of these analyses are often performed through abstract interpretation. We present a new termination analysis which integrates the various components and produces a set of constraints that, when solvable, identifies successful termination proofs. The proposed method is both efficient and precise. The use of constraint sets enables the propagation on information over all different phases while the need for multiple analyses is considerably reduced.

Given a program and some input data, partial deduction computes a specialized program handling any remaining input more efficiently. However, controlling the process well is a rather difficult problem. In this article, we elaborate global control for partial deduction: for which atoms, among possibly infinitely many, should specialized relations be produced, meanwhile guaranteeing correctness as well as termination? Our work is based on two ingredients. First, we use the concept of a characteristic tree, encapsulating specialization behavior rather than syntactic structure, to guide generalization and polyvariance, and we show how this can be done in a correct and elegant way. Second, we structure combinations of atoms and associated characteristic trees in global trees registering “causal” relationships among such pairs. This allows us to spot looming nontermination and perform proper generalization in order to avert the danger, without having to impose a depth bound on characteristic trees. The practical relevance and benefits of the work are illustrated through extensive experiments. Finally, a similar approach may improve upon current (on-line) control strategies for program transformation in general such as (positive) supercompilation of functional programs. It also seems valuable in the context of abstract interpretation to handle infinite domains of infinite height with more precision.

In [23] we presented a partial evaluation scheme for a "real tomatically generating highly specialised update procedures for deductive databases.

Recently, Gelfond and Lifschitz presented a formal language for representing incomplete knowledge on actions and states, and a sound translation from this language to extended logic programming. We present an alternative translation to abductive logic programming with integrity constraints and prove the soundness and completeness. In addition, we show how an abductive procedure can be used, not only for explanation, but also for deduction and proving satisfiability under uncertainty. From a more general perspective, this work can be viewed as a—successful—experiment in the declarative representation of and automated reasoning on incomplete knowledge using abductive logic programming.