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 demo, which can be specified as follows.

demo(P',Q') iff  P' and Q' are names of object program P and query Q and there exists a substitution yel_sigma.GIF (63 bytes) with P yel_provabil.GIF (59 bytes) Qyel_sigma.GIF (63 bytes)

DemoII provides an implementation of demo 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 demo_fails(P', Q'), with the meaning that the query named by Q' must fail in the program named by P'. It can be used for expressing counterexamples to predicates and integrity constraints, which are evaluated in a "lazy" and incremental way.

Developed and maintained by Henning Christiansen and Davide Martinenghi, Roskilde University, Denmark

This page was last updated Friday, January 22, 1999