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

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.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11390/667567
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 4
social impact