We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator boolean OR and the logical relators = and not equal. It can be seen that the dual language involving the Boolean operator boolean AND and, again, the relators = and not equal, also admits a cubic-time satisfiability decision test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators subset of and not subset of, and the predicates 'square = circle divide' and 'DISJ(square, square)', meaning 'the argument is empty' and 'the arguments are disjoint sets', along with their opposites 'square not equal circle divide' and '(sic)DISJ(square, square)'. Those richer languages are 'polynomial maximal', in the sense that each language strictly containing either of them and whose formulae are conjunctions of literals has an NP-hard satisfiability problem.A generalized version of the two said satisfiability tests can treat the relator not subset of, though at the price of a worsening of the algorithmic complexity (from cubic to quintic time). (c) 2023 Elsevier B.V. All rights reserved.
Complexity assessments for decidable fragments of Set Theory. III: Testers for crucial, polynomial-maximal decidable Boolean languages
Omodeo, EUltimo
Membro del Collaboration Group
2023-01-01
Abstract
We continue our investigation aimed at spotting small fragments of Set Theory (in this paper, sublanguages of Boolean Set Theory) that might be of use in automated proof-checkers based on the set-theoretic formalism. Here we propose a method that leads to a cubic-time satisfiability decision test for the language involving, besides variables intended to range over the von Neumann set-universe, the Boolean operator boolean OR and the logical relators = and not equal. It can be seen that the dual language involving the Boolean operator boolean AND and, again, the relators = and not equal, also admits a cubic-time satisfiability decision test; noticeably, the same algorithm can be used for both languages. Suitable pre-processing can reduce richer Boolean languages to the said two fragments, so that the same cubic satisfiability test can be used to treat the relators subset of and not subset of, and the predicates 'square = circle divide' and 'DISJ(square, square)', meaning 'the argument is empty' and 'the arguments are disjoint sets', along with their opposites 'square not equal circle divide' and '(sic)DISJ(square, square)'. Those richer languages are 'polynomial maximal', in the sense that each language strictly containing either of them and whose formulae are conjunctions of literals has an NP-hard satisfiability problem.A generalized version of the two said satisfiability tests can treat the relator not subset of, though at the price of a worsening of the algorithmic complexity (from cubic to quintic time). (c) 2023 Elsevier B.V. All rights reserved.File | Dimensione | Formato | |
---|---|---|---|
Complexity-assessments-for-decidable-fragments-of-Set-Theo_2023_Theoretical-.pdf
accesso aperto
Tipologia:
Documento in Versione Editoriale
Licenza:
Creative commons
Dimensione
546.86 kB
Formato
Adobe PDF
|
546.86 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.