DeReS (default reasoning system)
DeReS is an automated reasoning system based
on default logic. DeReS computes extensions
of default theories and stable models of logic programs. It can be regarded
as an implementation of the Answer Set Programming
Paradigm.
Several versions of DeReS are available. They include
-
lderes
lderes can process arbitrary default theories in the original DeReS
syntax. It is also possible to use lderes for programs in the logic programming
syntax (smodels version). To this end one
needs first to convert from smodels syntax
to DeReS syntax using a program sm2dt. lderes
was developed by Matt Levy who based his work on an earlier implementation
by Pawel Cholewinski. Relaxed stratification is used as the main pruning
mechanism.
-
sderes
sderes is also based on the original implementation
of DeReS by Pawel Cholewinski. It was built by Neil Moore. sderes computes
stable models of logic program. sm2dt
is needed in order to convert from the smodels syntax to the DeReS syntax.
Programs computing stratification are also available with sderes. They
improve the performance of the system.
-
stable
stable is a close derivative of smodels. The
main difference is in the heuristic choice of the next atom on which to
split. stable uses stratification to select an atom for splitting when
propagation through constraints is no longer possible. stable was developed
by Neil Moore. It accepts smodels syntax.
All three programs require lparse
(developed by the smodels group) to perform grounding. All three programs
together with lparse and several additional programs computing stratification
and performing conversion from lparse output to DeReS syntax are available
in one package referred to as DeReS.
Download
DeReS