Solvable set/hyperset contexts: I. Some decision procedures for the pure,finite case

Hereditarily finite sets and hypersets are characterized both as algorithmic data structures and by means of a first-order axiomatization which, despite being rather weak, suffices to make the following two problems decidable:

• (1) Establishing whether a conjunction r of formulae of the form: ? y₁ ?? y_m((y₁?W₁& ?&y_m ?W_m) ←q), with q quantifier-free and involving only the relators =, ? and propositional connectives, and each y_i distinct from all w_j's, is satisfiable.
• (2) Establishing whether a formula of the form ? y q, q quantifier-free, is satisfiable.

Concerning (1), an explicit decision algorithm is provided; moreover, significantly broad subproblems of (1) are singled out in which a classification — that we call the ‘syllogistic decomposition’ of r — of all possible ways of satisfying the input conjunction r can be obtained automatically. For one of these subproblems, carrying out the decomposition results in a finite family of syntactic substitutions that generate the space of all solutions to r. In this sense, one has a unification algorithm. Concerning (2), a technique is provided for reducing it to a subproblem of (1) for which a decomposition method is available. The algorithmic complexity of the problems under study is highlighted; a generalization of the decidability results to a theory where sets are blended with free Herbrand functors is announced. © 1996 John Wiley & Sons, Inc.