Transformation-Based Bottom-Up Computation of the Well-Founded Model

We present a bottom-up algorithm for the computation of the well-founded model of non-disjunctive logic programs. Our method is based on the elementary program transformations studied by Brass and Dix [BD94, BD97, BD98a]. However, their "residual program" can grow to exponential size, whereas for function-free programs our "program reminder" is always polynomial in the size of the extensional database (EDB). As in the SLG-resolution of Chen and Warren [CW93, CW96, CSW95], we do not only delay negative but also positive literals if they depend on delayed negative literals. When disregarding goal-directedness, which needs additional concepts, our approach can be seen as a simplified bottom-up version of SLG-resolution applicable to range-restricted Datalog programs. Since our approach is also closely related to the alternating fixpoint procedure [VG89, VG93], it can possibly serve as a basis for an integration of the resolution-based, fixpoint-based, and transformation-based evaluation methods