We carry on a long-standing investigation aimed at identifying fragments of set theory that are potentially useful in automated verification with proof-checkers, such as ÆtnaNova, based on the set-theoretic formalism. This note provides a complete taxonomy of the polynomial and the NP-complete fragments consisting of all conjunctions that involve, besides variables intended to range over the von Neumann set-universe, a collection of constructs drawn from the Boolean set operators ∪,∩,∖ and the membership relators ∈ and ∉. This is done in sight of combining the aforementioned taxonomy with one recently put together for analogous fragments involving, in place of the relators ∈ and ∉, the Boolean relators ⊆,= and the predicates ‘⋅=∅’ and ‘Disj(⋅,⋅)’ (respectively meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’), along with their opposites ‘⊈,≠,⋅≠∅’ and ‘¬Disj(⋅,⋅)’.
Complexity assessments for decidable fragments of set theory. II: A taxonomy for ‘small’ languages involving membership
Cantone D.
;Maugeri P.;
2020-01-01
Abstract
We carry on a long-standing investigation aimed at identifying fragments of set theory that are potentially useful in automated verification with proof-checkers, such as ÆtnaNova, based on the set-theoretic formalism. This note provides a complete taxonomy of the polynomial and the NP-complete fragments consisting of all conjunctions that involve, besides variables intended to range over the von Neumann set-universe, a collection of constructs drawn from the Boolean set operators ∪,∩,∖ and the membership relators ∈ and ∉. This is done in sight of combining the aforementioned taxonomy with one recently put together for analogous fragments involving, in place of the relators ∈ and ∉, the Boolean relators ⊆,= and the predicates ‘⋅=∅’ and ‘Disj(⋅,⋅)’ (respectively meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’), along with their opposites ‘⊈,≠,⋅≠∅’ and ‘¬Disj(⋅,⋅)’.File | Dimensione | Formato | |
---|---|---|---|
Cantone2020_Article_ComplexityAssessment.pdf
solo gestori archivio
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
521.73 kB
Formato
Adobe PDF
|
521.73 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.