Differences

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

--- sav08:atomic_diagram_normal_form [2009/05/12 22:43]
vkuncak
+++ sav08:atomic_diagram_normal_form [2009/05/12 23:29]
vkuncak
@@ Line 2: / Line 2: @@
 We next consider a syntactic normal form that helps us understand the decidability of the combination problem.
 ===== Flat Form =====
@@ Line 21: / Line 22: @@
     C[t] \ \ \leadsto \ \ (x=t) \land C[x]
 \]
+**Example:** Represent  $f(x)+y < z$ as
+\[
+    x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z
+\]
 ===== Finiteness of Flat Literals with Fixed Variables =====
@@ Line 28: / Line 36: @@
 Assume $K$ variables. ($K = |FV(C)|$)
-Number of $R(y_1,\ldots,y_n) = K^n$
+Number of $R(y_1,\ldots,y_n)$ is: $K^n$
+Number of $x=y$ atomic formulas is: $K^2$
-Number of $x=y$ atomic formulas: $K^2$
+Number of $x=f(y_1,\ldots,y_n)$ literals is: $K^{n+1}$
-Number of $x=f(y_1,\ldots,y_n)$ literals: $K^(n+1)$
+Note: if we did **not** have only flat literals, we could have infinitely many atomic formulas, because of arbitrarily large terms.
-Note: if we did not have only flat literals, we could have infinitely many atomic formulas, because of arbitrarily large terms.
+**Example:** When we have relation symbols $<$ and no function symbols, and consider 3 variables $x$,$y$,$z$, possible atomic formulas are:
+  * $x=x$, $y=y$, $z=z$, $x=y$, $y=x$, $x=z$, $z=x$, $y=z$, $z=y$
+  * $x<x$, $y<y$, $z<z$, $x<y$, $y<x$, $x<z$, $z<x$, $y<z$, $z<y$
 ===== Atomic Diagram Normal Form =====