We recently undertook an investigation aimed at identifying small fragments of set theory (which in most cases are sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this note we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, , the Boolean relators ⊆, /⊆, =, /=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘· /= ∅’ and ‘¬Disj(·, ·)’.
Polynomial-time satisfiability tests for boolean fragments of set theory
Omodeo E.
2019-01-01
Abstract
We recently undertook an investigation aimed at identifying small fragments of set theory (which in most cases are sublanguages of Multi-Level Syllogistic) endowed with polynomial-time satisfiability decision tests, potentially useful for automated proof verification. Leaving out of consideration the membership relator ∈ for the time being, in this note we provide a complete taxonomy of the polynomial and the NP-complete fragments involving, besides variables intended to range over the von Neumann set-universe, the Boolean operators ∪, ∩, , the Boolean relators ⊆, /⊆, =, /=, and the predicates ‘· = ∅’ and ‘Disj(·, ·)’, meaning ‘the argument set is empty’ and ‘the arguments are disjoint sets’, along with their opposites ‘· /= ∅’ and ‘¬Disj(·, ·)’.File | Dimensione | Formato | |
---|---|---|---|
paper22.pdf
accesso aperto
Descrizione: Copyright © 2019 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.
Tipologia:
Documento in Versione Editoriale
Licenza:
Digital Rights Management non definito
Dimensione
639.56 kB
Formato
Adobe PDF
|
639.56 kB | Adobe PDF | Visualizza/Apri |
CEUR-WS.org_Vol-2396 - 34th Italian Conference on Computational Logic.pdf
accesso aperto
Descrizione: index Copyright © 2019 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.
Tipologia:
Documento in Versione Editoriale
Licenza:
Digital Rights Management non definito
Dimensione
26.27 kB
Formato
Adobe PDF
|
26.27 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.