We present a framework for expressing bottom-up algorithms to compute the well-founded model of non-disjunctive logic programs. Our method is based on the notion of conditional facts and elementary program transformations studied by BRASS and DIX (Brass and Dix, 1994; Brass and Dix, 1999) for disjunctive programs. However, even if we restrict their framework to nondisjunctive programs, their ‘residual program’ can grow to exponential size, whereas for function-free programs our ‘program remainder’ is always polynomial in the size of the extensional database (EDB). We show that particular orderings of our transformations (we call them strategies) correspond to well-known computational methods like the alternating fixpoint approach (Van Gelder, 1989; Van Gelder, 1993), the well-founded magic sets method (Kemp et al., 1995) and the magic alternating fixpoint procedure (Morishita, 1996). However, due to the confluence of our calculi (first noted in Brass and Dix, 1998), we come up with computations of the well-founded model that are provably better than these methods. In contrast to other approaches, our transformation method treats magic set transformed programs correctly, i.e. it always computes a relevant part of the well-founded model of the original program. These results show that our approach is a valuable tool to analyze, compare, and optimize existing evaluation methods or to create new strategies that are automatically proven to be correct if they can be described by a sequence of transformations in our framework. We have also developed a prototypical implementation. Experiments illustrate that the theoretical results carry over to the implemented prototype and may be used to optimize real life systems.

In Ferrucci, Pacini and Sessa (1995) an extended form of resolution, called Reduced SLD resolution (RSLD), is introduced. In essence, an RSLD derivation is an SLD derivation such that redundancy elimination from resolvents is performed after each rewriting step. It is intuitive that redundancy elimination may have positive effects on derivation process. However, undesiderable effects are also possible. In particular, as shown in this paper, program termination as well as completeness of loop checking mechanisms via a given selection rule may be lost. The study of such effects has led us to an analysis of selection rule basic concepts, so that we have found convenient to move the attention from rules of atom selection to rules of atom scheduling. A priority mechanism for atom scheduling is built, where a priority is assigned to each atom in a resolvent, and primary importance is given to the event of arrival of new atoms from the body of the applied clause at rewriting time. This new computational model proves able to address the study of redundancy elimination effects, giving at the same time interesting insights into general properties of selection rules. As a matter of fact, a class of scheduling rules, namely the specialisation independent ones, is defined in the paper by using not trivial semantic arguments. As a quite surprising result, specialisation independent scheduling rules turn out to coincide with a class of rules which have an immediate structural characterisation (named stack-queue rules). Then we prove that such scheduling rules are tolerant to redundancy elimination, in the sense that neither program termination nor completeness of equality loop check is lost passing from SLD to RSLD.

The well-founded semantics is one of the most widely studied and used semantics of logic programs with negation. In the case of finite propositional programs, it can be computed in polynomial time, more specifically, in O([mid ]At(P)[mid ] × size(P)) steps, where size(P) denotes the total number of occurrences of atoms in a logic program P. This bound is achieved by an algorithm introduced by Van Gelder and known as the alternating-fixpoint algorithm. Improving on the alternating-fixpoint algorithm turned out to be difficult. In this paper we study extensions and modifications of the alternating-fixpoint approach. We then restrict our attention to the class of programs whose rules have no more than one positive occurrence of an atom in their bodies. For programs in that class we propose a new implementation of the alternating-fixpoint method in which false atoms are computed in a top-down fashion. We show that our algorithm is faster than other known algorithms and that for a wide class of programs it is linear and so, asymptotically optimal.

This note illustrates theoretical worst-case scenarios for groundness analyses obtained through abstract interpretation over the abstract domains of definite (Def) and positive (Pos) Boolean functions. For Def, an example is given for which any Def-based abstract interpretation for groundness analysis follows a chain which is exponential in the number of argument positions as well as in the number of clauses but sub-exponential in the size of the program. For Pos, we strengthen a previous result by illustrating an example for which any Pos-based abstract interpretation for groundness analysis follows a chain which is exponential in the size of the program. It remains an open problem to determine if the worst case for Def is really as bad as that for Pos.

Imperative programmers often use cyclically linked trees in order to achieve O(1) navigation time to neighbours. Some logic programmers believe that cyclic terms are necessary to achieve the same in logic-based languages. An old but little-known technique provides O(1) time and space navigation without cyclic links, in the form of reversible predicates. A small modification provides O(1) amortised time and space editing.

Submission deadline: January 10, 2002

The past decade has seen dramatic growth in the application of model checking techniques to the validation and verification of correctness properties of hardware, and more recently software systems. One of the methods is to model a hardware or software system as a finite, labelled transition system which is then exhaustively explored to decide whether a given temporal specification holds. Recently, there has been increasing interest in applying logic programming techniques to model checking in particular and verification in general. For example, table-based logic programming can be used as an efficient means of performing explicit model checking. Other research has successfully exploited set-based logic program analysis, constraint logic programming, and logic program transformation techniques.

The aim of this special issue is to attract high-quality research papers on the interplay between verification techniques (e.g. model checking, reduction and abstraction) and logic programming techniques (e.g. constraints, abstract interpretation, program transformation).