Affiliations: [a] Dept. of Mathematics and Computer Science, University of Catania, Italy. [email protected] | [b] Scuola Superiore di Catania, University of Catania, Italy. [email protected] | [c] Dept. of Mathematics and Computer Science, University of Catania, Italy. [email protected] | [d] Dept. of Mathematics and Geosciences, University of Trieste, Italy. [email protected]
Correspondence:
[†]
Address for correspondence: DMI, Università degli Studi di Catania, viale Andrea Doria, 6 – 95125 – Catania (I), Italy
Note: [*] We gratefully acknowledge partial support from project “STORAGE—Università degli Studi di Catania, Piano della Ricerca 2020/2022, Linea di intervento 2”, and from INdAM-GNCS 2019 and 2020 research funds.
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.
Keywords: Satisfiability problem, Computable set theory, Boolean set theory, Expressibility, NP-completeness, Proof verification
