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
- S. Brass, J. Dix:
Disjunctive Semantics Based upon Partial and Bottom-Up Evaluation.
Proc. 12th Int. Conf. on Logic Programming, MIT, 1995, 199-213.
- S. Brass, J. Dix, I. Niemelä, T. Przymusinski:
A Comparison of STATIC Semantics with D-WFS
Research Report 2 1996 (Abstract,
Report)
To appear in the Proc. of ILPS '97
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
Usage
Start the program by either calling
if you have a command-line version of the program, or loading
dwfs_mm into ECLiPSe Prolog and then running it:
| [dwfs_mm]. |
| dwfs_mm(<Filename>). |
|
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:
- Literals can be either atoms or otherwise ground terms.
- Express the negation of a literal a either as
not(a), !a or -a. In clauses,
negative literals can appear only in the body.
- Separate left-hand and right-hand side of a clause by
"<-", use semicolons for disjunctions and commas for
conjunctions, e.g.
a ; b ; c <- d , not e.
- Empty clause heads are represented by false. Empty
clause bodies are represented by true.
Besides clauses, two other elements may be present in the input file:
- a query - only one per input file - preceded by "?-" and
consisting of a disjunction
either of positive or of negative literals, e.g.
?- a ; b ; c
and
- terms of the form
problem_info(T).
where T is either a ground term or a string. T will
appear in the output messages at the end of the proof
process. Use this command for problem descriptions. You can
place any number of these in the input file.
Back to the DisLoP
home page.
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 $