mm: an implementation for
minimal model and circumscriptive reasoning
DisLoP Home *
dwfs *
dwfs_mm *
cdwfs *
test cases
mm is an implementation of the tableau-based method for automating
minimal model and circumscriptive reasoning. This system has been
developed as a part of the research project
DisLoP
funded by
DFG.
This system has been described in detail in:
- Ilkka Niemelä,
A tableau calculus for minimal model reasoning.
Research Report 5-96, Universität Koblenz-Landau, 1996.
(Abstract,
Report)
Appears in the
Proceedings of the Fifth Workshop on Theorem Proving with
Analytic Tableaux and Related Methods, Palermo, Italy, May 15-17,
1996, Springer-Verlag, 1996.
- Ilkka Niemelä,
Implementing Circumscription Using a Tableau Method.
Research Report 6-96, Universität Koblenz-Landau, 1996.
(Abstract,
Report)
Appears in the Proceedings of the European Conference on Artificial
Intelligence. Budapest, Hungary, Aug 12-16, 1996,
John Wiley, 1996.
mm accepts inputs in clausal form and implements parallel
circumscription in the propositional case: any combination of minimized,
fixed, and varying atoms is possible.
mm works as follows:
If a query is specified, then mm returns "query succeeded" if the
query is true in every minimal model of the given clauses (parallel
circumscription) and otherwise it returns one/all (depending on the
query mode) "counter-models" it finds (minimal models of the clauses
where the query is false).
If no query is given, mm returns one/all minimal models of the
clauses it finds.
mm is written in Eclipse Prolog by Ilkka Niemelä and
Katrin Erk.
The prototype implementation and some test cases are available as a
gzipped tar file.
For more details, see the
user's guide.
If you have questions or comments, please send an email to
Ilkka Niemelä or
Katrin Erk.
Examples
-
To compute all minimal models, one writes a file 'filename' with the
clauses and some declarations as follows:
a ; b ; c ; d <- true.
false <- a, c.
c <- a.
query_mode(all).
minimized(rest).
loads the file mm.pl to Eclipse and issues the call
mm('filename').
-
To decide whether a query
(a,-b);(-c,d)
(where ',' is conjunction, ';' is
disjunction and '-' is negation)
is true in all minimal models of
a set of clauses where a and b are fixed atoms and c is minimized, one
writes a file 'filename' with the clauses and some declarations as follows:
a ; b ; c ; d <- true.
false <- a, c.
c <- a.
query_mode(one).
fixed([a,b]).
minimized(c).
?- (a,-b);(-c,d).
and issues the call
mm('filename').
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:18:16 $