The DLS algorithm
Version 1.0 alpha
This is an alpha version of the DLS algorithm which we believe
to be stable and correct. This page and the algorithm should still
be considered under construction and subject to change. We would
appreciate feedback in any form and hope you find the algorithm
useful.
Please send any comments to
Joakim Gustafsson
at joagu@ida.liu.se.
The algorithm is implemented using
ECLiPSe,
the ECRC Constraint Logic Parallel System developed at ECRC, the
European Computer-Industry Research Centre GmbH.
This page contains the following sections:
- (2/01/96) This is version 1.0alpha of the DLS algorithm. We believe it to be stable and
correct, but both the web site and the implementation will be subject to
revision in the near future.
- We are currently working on a better way to simplify and present the output of
the algorithm, so please bear with us.
- Some minor bugs in the parser have now been fixed (16/04/97).
- The sift-procedure was extended to handle a broader class of problems (16/10/97).
- Serious bug dealing with minimization of multiple predicates in circumscription fixed (16/10/00).
The DLS algorithm was developed by Patrick Doherty, Witold Lukaszewicz, and
Andrzej Szalas.
The algorithm takes as input an arbitrary second-order formula and either returns
as output an equivalent first-order formula, or terminates with failure. Of course,
termination with failure does not imply that there isn't an equivalent first-order
formula. There are two reasons for termination: 1) there is no first-order equivalent,
or 2) there is but the algorithm can not generate it.
The algorithm is based on a generalization of Ackermann's Lemma, and has applications
in a number of areas, in particular, the reduction of circumscription axioms.
The following list contains a number of publications related to the DLS algorithm
and its extension:
-
Computing Circumscription Revisited: Preliminary Report, [c-ijcai-95-1502] (ps.gz file)
- Patrick Doherty, Witold Lukaszewicz, Andrzej Szalas.
- In Proceedings of the 14th Int'l Joint Conf. on Artificial Intelligence,
vol. 2, pp. 1502-1508.
- This provides a moderately detailed account of the DLS algorithm without
proofs and includes a few examples.
-
Computing Circumscription Revisited: A Reduction Algorithm, [j-jar-97-xxxx](ps.gz file)
- Patrick Doherty, Witold Lukaszewicz, Andrzej Szalas.
- Accepted for publication: Journal of Automated Reasoning, 1996.
- This is the most detailed published account of the DLS algorithm
with proofs and many examples.
-
General Domain Circumscription and its First-Order Reduction, [r-96-01.ps.gz]
- Patrick Doherty, Witold Lukaszewicz, Andrzej Szalas.
- Technical Report LiTH-IDA-R-96-01. Dept. of Computer and Information Science,
Linkoping University, Sweden, 1996.
- This report describes a generalization of domain circumscription and an
extension of the DLS algorithm used to reduce domain circumscription axioms.
- A revised and shorter version
[c-fapr-96-xxxx] (ps.gz file)
of this report has been accepted to the "Int'l Conf.
on Formal and Applied Reasoning" (FAPR'96), 1996, Bonn, Germany.
- An Implementation and Optimization of an Algorithm for Reducing Formulas
in Second-Order Logic.
- Joakim Gustafsson
- Technical Report LiTH-MAT-R-96-04. Dept. of Mathematics,
Linkoping University, Sweden, 1996.
- This report describes the current implementation of the DLS algorithm with
some additional optimizations. It is Joakim's final area study report for
his BSc degree.
We currently supply three forms for using the DLS algorithm. The first form should be used
when reducing arbitrary second-order formulas. The second form should be used when
reducing circumscription axioms. The third form should be used when reducing
nested circumscription theories.
- Use this form when reducing arbitrary second-order formulas.
- Here is an example run using the DLS algorithm.
- Use this form when reducing circumscription axioms.
- Use this form when reducing nested abnormality theories.
The DLS algorithm was constructed by:
The algorithm was implemented by Joakim Gustafsson.
If there are any questions about the program, or you have found an example that should work
using the DLS algorithm, but did not work using this implementation, please contact me at
joagu@ida.liu.se
You are the 
visitor to try out our algorithm.