Alternating Fixed Points in Boolean Equation Systems as Preferred Stable Models

Abstract:

We formally characterize alternating fixed points 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, and define a mapping that associates a normal logic program with a boolean equation system such that the solution to the equation system can be ``read off'' the preferred stable model of the logic program. We also show that the preferred model cannot be calculated a-posteriori (i.e. compute stable models and choose the preferred one) but rather must be computed in an intertwined fashion with the stable model itself. The mapping reveals a natural relationship between the evaluation of alternating fixed points in boolean equation systems and the Gelfond-Lifschitz transformation used in 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).

Bibtex Entry:

@inproceedings{KRS:ICLP01,
author = {K. Narayan Kumar and  C. R. Ramakrishnan and  Scott A. Smolka},
title = {Alternating Fixed Points in Boolean Equation Systems as Preferred Stable Models},
booktitle = {International Conference on Logic Programming ({ICLP})},
address = {Paphos, Cyprus},
month = {November},
series = {Lecture Notes in Computer Science},
volume = {2237},
publisher = {Springer},
pages = {227--241},
year = {2001}
}

Full Paper:

[pdf]

C. R. Ramakrishnan
(cram@cs.sunysb.edu)