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
Next revision Both sides next revision
sav08:solving_set_constraints_using_monadic_class [2008/05/22 00:18]
vkuncak 		sav08:solving_set_constraints_using_monadic_class [2008/05/22 13:19]
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 [[lecture23]]
 +
 +===== 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}}