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.
Transformation-based bottom-up computation of the well-founded model
