Solvable set/hyperset contexts: I. Some decision procedures for the pure, finite case
Eugenio Giovanni Omodeo, Alberto Policriti · Communications on Pure and Applied Mathematics · 1995
Abstract 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: Establishing whether a conjunctionrof formulae of the form: ∀ y1⃛∀ ym((y1ϵW1& ⃛&ymϵWm) ←q), withqquantifier‐free and involving only the relators =, ϵ and propositional connectives, and eachyidistinct from allwj's, is satisfiable. Establishing whether a formula of the form ∀y q, qquantifier‐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’ ofr— of all possible ways of satisfying the input conjunctionrcan 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 tor. 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.