Decidability of the Satisfiability Problem for Boolean Set Theory with the Unordered Cartesian Product Operator

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 ⊗ (where \(s \otimes t := \b...

Full description

Saved in:
Bibliographic Details
Published in:ACM transactions on computational logic 2024-01, Vol.25 (1), p.1-30, Article 5
Main Authors: Cantone, Domenico, Ursino, Pietro
Format: Article
Language:English
Subjects:
Automated reasoning
Theory of computation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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 ⊗ (where \(s \otimes t := \big \lbrace \lbrace u,v\rbrace \,\texttt {|}\:u \in s \wedge v \in t \big \rbrace\) ), 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.
ISSN:1529-3785
1557-945X
DOI:10.1145/3626823