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:logic_and_automata_introduction [2008/05/14 10:10]
vkuncak
sav08:logic_and_automata_introduction [2008/05/14 11:06]
vkuncak
Line 1: Line 1:
-====== Logic and Automata Introduction ======+====== Logic and Automata ​Introduction ======
  
 Satisfiability of $F$: is there an interpretation in which $F$ is true. Satisfiability of $F$: is there an interpretation in which $F$ is true.
Line 14: Line 14:
 More generally, for each formula with free variables, we compute the relation that the formula defines. More generally, for each formula with free variables, we compute the relation that the formula defines.
  
-Example: compute ​the unary relation (set) corresponding to this formula $F(z)$:+=== Example ​=== 
 + 
 +Compute ​the unary relation (set) corresponding to this formula $F(z)$:
 \[ \[
    ​\exists x. \exists y.\ z = 2 x + 1 \land z = 3 y + 2    ​\exists x. \exists y.\ z = 2 x + 1 \land z = 3 y + 2
 \] \]
 ++++| ++++|
-Add 6k to solution, we obtain a solution.+Add 6k to solution, we obtain a solution. ​\\
  
-Find solutions in set $\{0,​1,​2,​3,​4,​5\}$+Find solutions in set $\{0,​1,​2,​3,​4,​5\}$. \\
  
-Resulting relation for $F(z)$ is $\{ 6k + 5 \mid k \in \mathbb{Z} \}$+Resulting relation for $F(z)$ is $\{ 6k + 5 \mid k \in \mathbb{N} \}$. \\ 
 + 
 +Representation as quantifier-free formula. \\ 
 + 
 +Representation as a regular language.
 ++++ ++++
 +
 +===== Basic Idea =====
 +
 +We come up with a '​nice'​ //​representation//​ of relations
 +  * in quantifier elimination these are particular quantifier-free formulas
 +  * in automata-based methods that we will look at, we represent relations as regular languages
  
 In [[Lecture15]] we have seen that Presburger arithmetic is decidable using quantifier elimination.  ​ In [[Lecture15]] we have seen that Presburger arithmetic is decidable using quantifier elimination.  ​
  
-Today we look at a different ​decision method ​for Presburger arithmetic, ​which generalizes ​to certain ​more expressive logics ​(monadic second-order logic over strings and trees).+Today we see an alternative ​decision method, based on Presburger arithmetic, ​and then generalize it to more expressive logicsmonadic second-order logic over strings and trees.