Decision Algorithms for a Class of Set-Theoretic Formulae Involving One Occurrence of the Union-Set Operator

Candidate: Breban,Michael


We consider the first order language allowing the operators = (equality), (epsilon) (membership), (UNION) (binary union), (INTERSECT) (binary intersection), (FDIAG) (set difference), { } (singleton former) and one occurrence of Un (unary union). We show that unquantified formulae of this language are decidable. As a preparatory result we show that unquantified formulae of the above mentioned language not involving the singleton former are decidable.