# Solving Set Constraints using Monadic Class

## Definition of Monadic Class of FOL

**Definition:** The class of first-order logic formulas in the language that contains only unary predicates.

Decidability: special case of first-order theory of Boolean Algebras, or WS1S, so it can be decided using techniques we have seen:

- Deciding MSOL over Strings and Trees in Lecture 15

## Equisatisfiability of Monadic Class and Set Constraints

If we take a formula in monadic class and

- flatten
- skolemize
- look at Herbrand universe

Then we obtain set constraints.

Converse is also true: for every set constraint there exists a corresponding formula in monadic class.