Embedding extensional finite sets in CLP

In this paper we review the definition of {log}, a logic language with sets, from the viewpoint of CLP. We show that starting with a CLP-scheme allows a more uniform treatment of the built-in set operations (namely, =, ∈ and their negative counterparts), and allows all the theoretical results of CLP to be immediately exploitable. We prove this by precisely defining the privi- leged interpretation domain and the axioms of the selected set theory. Then we define a non-deterministic procedure for checking constraint satisfiability based on the reduction of a given constraint to a collection of constraint in a suitable canonical form, which is provable to be sound and complete w.r.t. the given theory. Algorithms for trasforming each one of the set constraints the language provides (=, ̸=, ∈ and ̸∈) into their corresponding canonical forms are described in details. It is also shown that the resulting language is powerful enough to allow all the usual operations on sets (such as ⊆, ∪, etc.) to be effectively programmed in the language itself.