The time complexity of well-founded semantics for a general logic program **P** is known to be quadratic in the size of **P**, a result attributed to folklore in [1]. A proof was given by Witteveen (1991). His analysis is based on Dowling and Gallier's result whereby satisfiability of Horn clauses can be tested in linear time [6]. In Dowling and Gallier's approach it is actually a minimal model of a Horn theory that is computed in linear time. Since minimal models of Horn theories are equivalent to closures of rules without negation the result is directly applicable to well-founded semantics for general logic programs. It also applies to well-founded semantics for extended logic programs since for the computation of the least fixed point of respectively the complementary literals **l** and can be vi
wed as two distinct atoms.

For the complexity analysis of our prioritized approach let **n** be the number of rules in a prioritized program .
A straightforward implementation would model the application of in an outer loop and the computation of in an inner loop. Fortunately, we can combine the two loops into a single loop whose body is executed at most **n** times. The reason is that grows monotonically with **X** and grows monotonically with . Here is a nondeterministic algorithm for computing the least fixed point of :

In each step and denote the well-founded conclusions, respectively safe rules established so far. The body of the for-loop is executed at mostProcedureWFS+

Input:A prioritized logic program with|R| = n

Output:the least fixed point of

;

;

fori = 1tondoif there is a rule such thatendfor

does not defeatr

then

else return

endWFS+

More precisely, Dowling and Gallier show that the needed time is linear in the number of propositional constants. This number may be greater than **n** in principle. However, since literals that do not appear in the head of a rule must be false in the minimal model we can eliminate them accordingly and work with a set of rules that has at most **n** literals. This leads to an overall time complexity of .

It should be mentioned, however, that due to the use of rule schemata for transitivity and anti-symmetry of prioritized programs can be considerably larger than corresponding unprioritized programs. The transitivity schema, for instance, has instances. An implementation should, therefore, be based on an approach where instances are only generated when actually needed, or on other built in techniques that handle transitivity and anti-symmetry. Such techniques are beyond the scope of this paper.

Thu Feb 8 10:26:15 MET 1996