The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the There Exists*For All class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented.
Decidability of E*A-sentences in Membership Theories
PARLAMENTO, Franco;POLICRITI, Alberto
1996-01-01
Abstract
The problem is addressed of establishing the satisfiability of prenex formulas involving a single universal quantifier, in diversified axiomatic set theories. A rather general decision method for solving this problem is illustrated through the treatment of membership theories of increasing strength, ending with a subtheory of Zermelo-Fraenkel which is already complete with respect to the There Exists*For All class of sentences. NP-hardness and NP-completeness results concerning the problems under study are achieved and a technique for restricting the universal quantifier is presented.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
final.pdf
accesso aperto
Tipologia:
Documento in Post-print
Licenza:
Non pubblico
Dimensione
1.01 MB
Formato
Adobe PDF
|
1.01 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
