Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:atomic_diagram_normal_form [2009/05/12 23:24] vkuncak |
sav08:atomic_diagram_normal_form [2009/05/12 23:30] vkuncak |
||
|---|---|---|---|
| Line 27: | Line 27: | ||
| x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z | x_1 = f(x) \land s_1 = x_1 + y \land s_1 < z | ||
| \] | \] | ||
| + | |||
| + | |||
| + | |||
| ===== Finiteness of Flat Literals with Fixed Variables ===== | ===== Finiteness of Flat Literals with Fixed Variables ===== | ||
| Line 40: | Line 43: | ||
| Number of $x=f(y_1,\ldots,y_n)$ literals is: $K^{n+1}$ | Number of $x=f(y_1,\ldots,y_n)$ literals is: $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$ | ||
| + | and there are 3^2+3^2=18 atomic formulas. | ||
| ===== Atomic Diagram Normal Form ===== | ===== Atomic Diagram Normal Form ===== | ||