(LOG) - A LANGUAGE FOR PROGRAMMING IN LOGIC WITH FINITE SETS

An extended logic programming language is presented, that embodies the fundamental form of set designation based on the (nesting) element in sertion operator. The kind of sets to be handled is characterized both by adaptation of a suitable Herbrand universe and via axioms. Predica tes is an element of and = designating set membership and equality are included in the base language, along with their negative counterparts is not an element of and not equal. A unification algorithm that can cope with set terms is developed and proved correct and terminating. I t is proved that by incorporating this new algorithm into SLD resoluti on and providing suitable treatment of is an element of, not equal, an d is not an element of as constraints, one obtains a correct managemen t of the distinguished set predicates. Restricted universal quantifier s are shown to be programmable directly in the extended language and t hus are added to the language as a convenient syntactic extension. A s imilar solution is shown to be applicable to intensional set-formers, provided either a built-in set collection mechanism-or some form of ne gation in goals and clause bodies is made available.