Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case*
| Autor: | Pietro Maugeri, Andrea De Domenico, Eugenio G. Omodeo, Domenico Cantone |
|---|---|
| Přispěvatelé: | Cantone, D., De Domenico, A., Maugeri, P., Omodeo, E. |
| Rok vydání: | 2021 |
| Předmět: |
Algebra and Number Theory
Theoretical computer science Computer science Computable set theory Boolean set theory Expressibility NP-completeness Proof verification Satisfiability problem NP-completene Theoretical Computer Science Decidability Computational Theory and Mathematics Taxonomy (general) Set theory Information Systems |
| Zdroj: | Fundamenta Informaticae. 181:37-69 |
| ISSN: | 1875-8681 0169-2968 |
| DOI: | 10.3233/fi-2021-2050 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|