FINDER (Finite Domain Enumerator)

John Slaney

These notes are taken from the introduction to the FINDER manual.
The manual comes with the package, or it can be downloaded separately (postscript)
The program is available, in a somewhat upgraded version. It is suggested that if you install or use FINDER you let us know that you have it, so that we can distribute information about updates, patches, etc. to as many sites as possible.

The program FINDER (Finite Domain Enumerator) takes as input a first order theory, expressed as a set of clauses, and gives as output the models of that theory with domains of given finite cardinality (up to a maximum size of 31). It can be used for various kinds of problem-solving, or to generate counter-examples refuting conjectures, or in combination with other reasoning systems. For example, it may help to make proof searches more efficient by providing semantic information to a conventional deduction system.

FINDER performs an exhaustive search for interpretations of the given language, using the given clauses as constraints to direct its backtracking. One of the main differences between FINDER and a logic programming system (which can also be seen as searching for models of sets of clauses) is that for FINDER there is no order of evaluation of the clauses and hence no ``flow of control" such as underlies the operational semantics of conventional systems like Prolog. A model is generated and tried against all the clauses together; if all clauses are true, the model is accepted and printed out, while if one of the clauses is false the model is adjusted to deal with the detected badness, resulting in a further candidate model. This process goes on until enough models have been found or until the search space, defined as the set of possible interpretations of the predicate and function symbols on the chosen domain, is exhausted. The other principal difference between FINDER's kind of model-generation and that associated with more deduction-oriented techniques is that for FINDER the domain of individuals is given antecedently and is not constructed from the terms of the language. The objects in, say, a three-element domain are simply the first object, the second object, and the third object. They need not have names.

The code actually used by FINDER to control the search is exactly the same as that used by the earlier program MaGIC. In a straightforward sense, the problems treated by MaGIC may be seen as special cases of those treated by FINDER.

Automated Reasoning Group
Computer Sciences Laboratory
Research School of Information Sciences and Engineering
Australian National University