Differences

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

--- sav08:logic_and_automata_introduction [2008/05/14 10:12]
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.
@@ Line 14: / Line 14: @@
 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
 \]
 ++++|
-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.
 ++++
-We need a nice //representation// of relations
+===== 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