The Mathematics of Set Predicates in Prolog

We provide a logical speci cation of set predicates ndall and bagof of Prolog. The speci cation is given in proof theoretic terms, and pertains to any SLD resolution based language. The order dependent aspects, relevant for languages embodying a sequential proof search strategy possibly with side e ects, can be added in an orthogonal way. The speci cation also allows us to prove that bagof cannot be de ned by SLD resolution alone. We show the correctness, wrt to our speci cation, of Demoen's de nition of bagof for Prolog in Prolog. The speci cation of bagof allows us to throw some light on the logical problems with setof.

• Type: Conference
• Year: 1993
• Where: KGC
• Authors: Egon Börger, Dean Rosenzweig
• Keywords: Automated Reasoning, KGC 1993, Logical Speci Cation, SLD Resolution, Speci Cation