We give a positive solution to the decidability problem for the fragment of set theory, dubbed BST⊗, consisting of quantifier-free formulae involving the Boolean set operators of union, intersection, and set difference, along with the unordered Cartesian product operator ⊗, and the equality predicate, but no membership. Specifically, we provide nondeterministic exponential decision procedures for both the ordinary and the finite satisfiability problems for BST⊗. We expect that these decision procedures can be adapted for the standard Cartesian product and, with added technicalities, to the cases involving membership, providing a solution to a longstanding problem in computable set theory.
Decidability of the satisfiability problem for Boolean set theory with the unordered Cartesian product operator
Cantone, Domenico
;Ursino, Pietro
In corso di stampa
Abstract
We give a positive solution to the decidability problem for the fragment of set theory, dubbed BST⊗, consisting of quantifier-free formulae involving the Boolean set operators of union, intersection, and set difference, along with the unordered Cartesian product operator ⊗, and the equality predicate, but no membership. Specifically, we provide nondeterministic exponential decision procedures for both the ordinary and the finite satisfiability problems for BST⊗. We expect that these decision procedures can be adapted for the standard Cartesian product and, with added technicalities, to the cases involving membership, providing a solution to a longstanding problem in computable set theory.File | Dimensione | Formato | |
---|---|---|---|
3626823.pdf
accesso aperto
Tipologia:
Documento in Pre-print
Licenza:
Creative commons
Dimensione
393.41 kB
Formato
Adobe PDF
|
393.41 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.