Research in  Logic Programming

{log}: Constraint Logic Programming with
Finite Sets


Author(s)
Agostino Dovier @ the University of Pisa (Italy),
Eugenio G. Omodeo @ the University of Salerno (Italy),
Enrico Pontelli @ New Mexico State University
GianFranco Rossi @ the University of Parma (Italy)

Description
An extended logic programming language is presented, that embodies the fundamental form of set designation based on the (nesting) element insertion construct. The kind of sets to be handled is characterized both in concrete terms (i.e., by adaptation of a suitable Herbrand universe) and via axioms. Predicates \in,= designating set membership and equality are included in the base language along with their negative counterparts \neq and \notin. A goal-driven unification algorithm which can cope with set terms is developed and shown to terminate. It is then proved that by incorporating this new algorithm into SLD resolution, one properly manages the distinguished set predicates. Restricted universal quantifiers are introduced in the proposed language as a convenient syntactic extension, and the way is paved towards a similar (but more complex) introduction of intensional set-formers. It is in fact shown that the latter abstraction can be programmed directly in the extended language, provided either a built-in set collection mechanism or some form of negation in goals and clause bodies is made available. Implementations techniques are described, down to the level of a complete abstract machine ---{WAM}--- able to support the language execution.

Related Papers