We report on an investigation aimed at identifying small fragments of set theory (typically, 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 paper 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(•, •)'. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.

Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case

Omodeo E.
2021-01-01

Abstract

We report on an investigation aimed at identifying small fragments of set theory (typically, 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 paper 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(•, •)'. We also examine in detail how to test for satisfiability the formulae of six sample fragments: three sample problems are shown to be NP-complete, two to admit quadratic-time decision algorithms, and one to be solvable in linear time.
File in questo prodotto:
File Dimensione Formato  
paper22FundamentaInformaticae201023.pdf

accesso aperto

Descrizione: final version at DOI: 10.3233/FI-2021-2050
Tipologia: Bozza finale post-referaggio (post-print)
Licenza: Digital Rights Management non definito
Dimensione 478.76 kB
Formato Adobe PDF
478.76 kB Adobe PDF Visualizza/Apri
cantone2021.pdf

Accesso chiuso

Tipologia: Documento in Versione Editoriale
Licenza: Copyright Editore
Dimensione 430.29 kB
Formato Adobe PDF
430.29 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

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: https://hdl.handle.net/11368/3004951
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 3
social impact