DemoII is a meta-logic programming system that covers a wide range of automated
reasoning tasks including abduction and induction. These tasks are specified in terms of declarative
meta-level statements using the proof predicate
which can be specified as follows.
Q'are names of object program
Qand there exists a substitution with
DemoII provides an implementation of
which is reversible in the sense that it works equally well for executing known
programs as well as for generating new programs that make given goals provable.
Specifications in DemoII may include also syntactic bias and integrity constraints. The system appears as a highly generic environment for experiments with different reasoning methods. Distinct for the DemoII system is the ease with which different methods can be combined, e.g., integrating abduction and induction with default rules.
These properties are obtained using constraint logic techniques implemented with the Constraint Handling Rules library included in SICStus Prolog 3.7, under which the system runs. Among the features are:
|A syntactically sugared notation which makes programming about the ground representation of object programs much easier.|
|A module system to manage collections of object programs.|
|A negative proof predicate |
Developed and maintained by Henning Christiansen and Davide Martinenghi, Roskilde University, Denmark
This page was last updated Friday, January 22, 1999