User Manual Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse




Conference Paper

Computing Stable Models by Program Transformation


Stuber,  Jürgen
Programming Logics, MPI for Informatics, Max Planck Society;

There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available

Stuber, J. (1994). Computing Stable Models by Program Transformation. In P. Van Hentenryck (Ed.), Proceedings of the 11th International Conference on Logic Programming (ICLP'94) (pp. 58-73). Cambridge, USA: MIT Press.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-AD6D-7
In analogy to the Davis-Putnam procedure we develop a new procedure for computing stable models of propositional normal disjunctive logic programs, using case analysis and simplification. Our procedure enumerates all stable models without repetition and without the need for a minimality check. Since it is not necessary to store the set of stable models explicitly, the procedure runs in polynomial space. We allow clauses with empty heads, in order to represent truth or falsity of a proposition as a one-literal clause. In particular, a clause of form $\mathop\sim A\rightarrow$ expresses that~$A$ is constrained to be true, without providing a justification for~$A$. Adding this clause to a program restricts its stable models to those containing~$A$, without introducing new stable models. Together with $A\rightarrow$ this provides the basis for case analysis. We present our procedure as a set of rules which transform a program into a set of solved forms, which resembles the standard method for presenting unification algorithms. Rules are sound in the sense that they preserve the set of stable models. A subset of the rules is shown to be complete in the sense that for each stable model a solved form can be obtained. The method allows for concise presentation, flexible choice of a control strategy and simple correctness proofs."