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.

The algorithm is implemented using ECLiPSe, the ECRC Constraint Logic Parallel System developed at ECRC, the European Computer-Industry Research Centre GmbH.

### Latest Information

• (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).

### Brief Summary of the DLS Algorithm

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.

### Documentation

The following list contains a number of publications related to the DLS algorithm and its extension:

### WWW Interface Forms

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.

### Authors

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.