dwfs_mm: an implementation of the D-WFS semantics
based on minimal model reasoning

DisLoP Home * mm * dwfs * cdwfs * test cases

dwfs_mm is an extension of the mm minimal model reasoner. It uses iterative minimal model reasoning to implement the D-WFS semantics. This system has been developed as a part of the research project DisLoP funded by DFG.

D-WFS and the method underlying dwfs_mm are described in

dwfs_mm accepts as its input a disjunctive propositional program with negative body literals. It partially evaluates the program, and based on the partially evaluated program P* it answers queries which can be disjunctions either of positive or negative literals.

A query Qp consisting of a disjunction of positive literals succeeds in D-WFS iff

P*p |= Qp
where P*p are the clauses in P* without negative body literals.

A query Qn consisting of a disjunction of negative literals succeeds in D-WFS iff

P* |=min Qn.

|=min is minimal model consequence where negative atoms are fixed and only NAF-consistent models are allowed.

If no query is entered, only the partially evaluated program P* is written out at the end of the proof process.

dwfs_mm has been written in ECLiPSe Prolog by Ilkka Niemelä and Katrin Erk. The prototype implementation and some test cases are available as a gzipped tar file.

If you have questions or comments, please send an email to Ilkka Niemelä or Katrin Erk


Start the program by either calling
dwfs_mm <Filename>
if you have a command-line version of the program, or loading dwfs_mm into ECLiPSe Prolog and then running it:
Messages at the end of the proof process will go to two places: First to the screen, then to a file with the same name as the input file with ".res" attached.

For clauses and queries, use the following syntax:

Besides clauses, two other elements may be present in the input file:

Back to the DisLoP home page.
Counter visitors since June 27, 1997.

Maintained by: K. Erk <katrin@informatik.uni-koblenz.de> and C. Aravindan <arvind@informatik.uni-koblenz.de>
$Author: arvind $ $Date: 1997/10/17 14:19:50 $