An extended logic programming language embodying sets is developed in successive stages, introducing at each stage simple set dictions and operations, and discussing their operational as well as declarative semantics. First, by means of special set terms added to definite Horn Clause logic, one is enabled to define enumerated sets. A new unification algorithm which can cope with set terms is developed and proved to terminate. Moreover, distinguished predicates representing set membership and equality are added to the base language along with their negative counterparts, and SLD resolution is modified accordingly. It is shown that the resulting language allows restricted universal quantifiers in goals and clause bodies to be defined quite simply within the language itself. Finally, abstraction set terms are made available as intensional designations of sets. It is shown that also such terms become directly definable within the language, provided the latter is endowed with negation, which may occur in goals and clause bodies.
