Embedding extensional finite sets in CLP

Abstract

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, =, 2 and their negative counterparts), and allows all the theoretical results of CLP to be immediately exploitable. We prove this by precisely defining the privileged 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 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 subset, union etc.)