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 
:
Procedure WFS+In each step
Input: A prioritized logic programwith |R| = n
Output: the least fixed point of
;
;
for i = 1 to n doif there is a ruleendforsuch that
does not defeat r
then
else return
end WFS+
and 
denote the well-founded conclusions, respectively safe rules established so far. The body of the for-loop is executed at most n times and there are at most n rules that have to be checked for satisfaction of the if-condition. The if-condition itself can, according to the results of Dowling and Gallier, be checked in linear time: we need to establish 
which involves the computation of a minimal model of the monotonic counterparts of 
. We then have to eliminate the rules dominated by r form 
and compute another minimal model to see whether r is defeated.
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.
