A Decision Procedure for a Class of Unquantified Formulae of Set Theory Involving the Powerset and Singleton Operators

Candidate: Cantone,Domenico A.

Abstract

The class of unquantified formulae of set theory involving Boolean opeators, the powerset and the singleton operators, and the equality and membership predicates is shown to have a solvable satisfiability problem. It is also shown that whenever a formula (phi) in the above class is satisfiable there exists a hereditarily finite model of (phi), where rank is bounded by a doubly exponential expression in the number of variables occurring in (phi).