LARA

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:

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.

References