LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav08:solving_set_constraints_using_monadic_class [2008/05/22 00:18]
vkuncak 		sav08:solving_set_constraints_using_monadic_class [2010/05/31 13:36]
vkuncak
Line 1: Line 1:
 ====== Solving Set Constraints using Monadic Class ====== ====== 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 Boolean Algebra with Presburger Arithmetic]]
 +  * Deciding MSOL over Strings and Trees in [[sav10:​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.
 +
 +===== References =====
  
   * {{:​bachmairetal93setconstraintsmonadicclass.ps|Bachmair,​ Ganzinger, Waldmann: Set constraints are the monadic class}}   * {{:​bachmairetal93setconstraintsmonadicclass.ps|Bachmair,​ Ganzinger, Waldmann: Set constraints are the monadic class}}