mm: an implementation for
minimal model and circumscriptive reasoning
DisLoP Home *
dwfs *
dwfs_mm *
cdwfs *
test cases
mm
is an implementation of the tableaubased 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 596, Universität KoblenzLandau, 1996.
(Abstract,
Report)
Appears in the
Proceedings of the Fifth Workshop on Theorem Proving with
Analytic Tableaux and Related Methods, Palermo, Italy, May 1517,
1996, SpringerVerlag, 1996.
 Ilkka Niemelä,
Implementing Circumscription Using a Tableau Method.
Research Report 696, Universität KoblenzLandau, 1996.
(Abstract,
Report)
Appears in the Proceedings of the European Conference on Artificial
Intelligence. Budapest, Hungary, Aug 1216, 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) "countermodels" 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.unikoblenz.de> and
C. Aravindan
<arvind@informatik.unikoblenz.de>
$Author: arvind $ $Date: 1997/10/17 14:18:16 $