Solvable set/hyperset contexts: I. Some decision procedures for the pure,finite case |
| |
Authors: | Eugenio G Omodeo Alberto Policriti |
| |
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: - (1) Establishing whether a conjunction r of formulae of the form: ? y1 ?? ym((y1?W1& ?&ym ?Wm) ←q), with q quantifier-free and involving only the relators =, ? and propositional connectives, and each yi distinct from all wj'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. |
| |
Keywords: | |
|
|