hide
Free keywords:
-
Abstract:
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
mofels 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 $ \sim A \rightarrow $ expresses
that $ A $ is contrained 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.
