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

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:

Latest Information

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.


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.

Related Work


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

You are the visitor to try out our algorithm.