Embedding finite sets in a logic programming language

A way of introducing simple (finite) set designations and operations as first-class objects of an (unrestricted) logic programming language is discussed from both the declarative and the operational semantics viewpoint. First, special set terms are added to definite Horn clause logic and an extended Herbrand Universe based on an axiomatic characterization of the kind of sets we are dealing with is defined accordingly. Moreover, distinguished predicates representing set membership and equality are added to the base language along with their negative counterparts (π and ). A new unification algorithm which can cope with set terms is developed and proved to terminate. Usual SLD resolution is modified so as to incorporate the new unification algorithm and to properly manage the distinguished predicates for set operations (in particular, conjunctions of atoms containing π and are dealt with as constraints, first reduced to a canonical form through a suitable canonization algorithm). Finally, the application of the resulting language to the definition of Restricted Universal Quantifiers is discussed.