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:

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.


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

    Maintained by: K. Erk <> and C. Aravindan <>
    $Author: arvind $ $Date: 1997/10/17 14:18:16 $