A Decision Procedure for Sets, Binary Relations and Partial Functions

In this paper we present a decision procedure for sets, binary relations and partial functions. The language accepted by the decision procedure includes untyped, hereditarily finite sets, where some of their elements can be variables, and basically all the classic set and relational operators used in formal languages such as B and Z. Partial functions are encoded as binary relations which in turn are just sets of ordered pairs. Sets are first-class entities in the language, thus they are not encoded in lower level theories. The decision procedure exploits set unification and set constraint solving as primitive features. The procedure is proved to be sound, complete and terminating. A Prolog implementation is presented.