We formally characterize alternating fixedp oints of boolean equation systems as models of (propositional) normal logic programs. To this end, we introduce the notion of a preferred stable model of a logic program, andd efine a mapping that associates a normal logic program with a boolean equation system such that the solution to the equation system can be “reado. ” the preferredstable model of the logic program. We also show that the preferredmo del cannot be calculateda-p osteriori (i.e. compute stable models andc hoose the preferredone) but rather must be computedin an intertwinedfashion with the stable model itself. The mapping reveals a natural relationship between the evaluation of alternating fixedp oints in boolean equation systems andthe Gelfond- Lifschitz transformation usedin stable-model computation.
For alternation-free boolean equation systems, we show that the logic programs we derive are stratified, while for formulas with alternation, the corresponding programs are non-stratified. Consequently, our mapping of boolean equation systems to logic programs preserves the computational complexity of evaluating the solutions of special classes of equation systems (e.g., linear-time for the alternation-free systems, exponential for systems with alternating fixed points).