Decision Procedures for some Classes of Unquantified Set Theoretic Formulae

Candidate: Ferro,Alfredo

Abstract

We consider the first order language consisting of = (equality), (ELEM) (membership), (UNION) (binary union), (INTERSECT) (binary intersection), (FDIAG) (set difference), and pow (powerset former). We show that the class of all universal sentences of this language is decidable, provided that we impose the strong restriction that at most two terms appear as arguments of the powerset former. As a preliminary result we show that the class of all universal sentences in the above language extended by allowing infinitely many constants: one for each hereditarily finite set, is decidable provided that we allow only a single occurrence of the powerset former.