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
- 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.