Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
expressing_regular_expressions_in_msol_over_strings [2007/05/06 21:01]
vkuncak
expressing_regular_expressions_in_msol_over_strings [2007/05/06 21:04] (current)
vkuncak
Line 10: Line 10:
   ... ...     ... ...   ... ...     ... ...
   ... apn ... aqn ...   ... apn ... aqn ...
 +
 +The construction is by induction on the structure of regular expressions and resembles the description of parsing the string given by a regular expression:
 +  * base cases are easy
 +  * union is disjunction
 +  * concatenation existentially quantifies over middle position
 +  * iteration in $r^*$ quantifies over a set of positions between $p$ and $q$ at which a string can be broken into strings that satisfy $r$
  
 
expressing_regular_expressions_in_msol_over_strings.txt · Last modified: 2007/05/06 21:04 by vkuncak
 
© EPFL 2018 - Legal notice