LARA

Differences

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

Link to this comparison view

sav08:logic_and_automata_introduction [2008/05/14 11:05]
vkuncak
sav08:logic_and_automata_introduction [2015/04/21 17:30]
Line 1: Line 1:
-====== Logic and Automata - Introduction ====== 
- 
-Satisfiability of $F$: is there an interpretation in which $F$ is true. 
- 
-Validity of $F$: is $F$ true in all interpretations (reduces to satisfiability of $\lnot F$). 
- 
-Some techniques for establishing this for quantified formulas: 
-  * quantifier elimination (seen before) 
-  * automata-based techniques - this lecture and next one 
-  * game-based techniques (perhaps next week) 
- 
-Common for quantifier elimination and automata-based techniques: characterize the set of all models (interpretations in which $F$ is true). 
- 
-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)$: 
-\[ 
-   ​\exists x. \exists y.\ z = 2 x + 1 \land z = 3 y + 2 
-\] 
-++++| 
-Add 6k to solution, we obtain a solution. \\ 
- 
-Find solutions in set $\{0,​1,​2,​3,​4,​5\}$. \\ 
- 
-Resulting relation for $F(z)$ is $\{ 6k + 5 \mid k \in \mathbb{Z} \}$. \\ 
- 
-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.  ​ 
- 
-Today we see an alternative decision method, based on Presburger arithmetic, and then generalize it to more expressive logics: monadic second-order logic over strings and trees.