SOLVABLE SET HYPERSET CONTEXTS .1. SOME DECISION PROCEDURES FOR THE PURE, FINITE CASE

Hereditarily finite sets and hypersets are characterized both as algor ithmic data structures and by means of a first-order axiomatization wh ich, despite being rather weak, suffices to make the following two pro blems decidable: (1) Establishing whether a conjunction r of formulae of the form: For All y(1) ... For All y(m) ((y(1) epsilon w(1) &...&y( m) epsilon w(m)) --> q), with q quantifier-free and involving only the relators =, epsilon and propositional connectives, and each y(i) dist inct from all w(j)'s, is satisfiable. (2) Establishing whether a formu la of the form For All y q, q quantifier-free, is satisfiable. Concern ing (1), an explicit decision algorithm is provided; moreover, signifi cantly broad subproblems of (1) are singled out in which a classificat ion - that we call the 'syllogistic decomposition' of r - of all possi ble ways of satisfying the input conjunction r can be obtained automat ically. For one of these subproblems, carrying out the decomposition r esults in a finite family of syntactic substitutions that generate the space of all solutions to r. In this sense, one has a unification alg orithm. Concerning (2), a technique is provided for reducing it to a s ubproblem of (1) for which a decomposition method is available. The al gorithmic complexity of the problems under study is highlighted; a gen eralization of the decidability results to a theory where sets are ble nded with free Herbrand functors is announced. (C) 1996 John Wiley & S ons, Inc.