Differences

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

--- sav08:atomic_diagram_normal_form [2009/05/12 23:30]
vkuncak
+++ sav08:atomic_diagram_normal_form [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Atomic Diagram Normal Form ======
-We next consider a syntactic normal form that helps us understand the decidability of the combination problem.
-===== Flat Form =====
-By introducing fresh variables, each conjunction of literals can be represented as an equisatisfiable conjunction of only "flat literals", which are flat atomic formulas or their negation, where flat atomic formula is
-\[
-   R(y_1,\ldots,y_n)
-\]
-\[
-    x = y
-\]
-\[
-    x = f(y_1,\ldots,y_n)
-\]
-We call this "flat form" of the conjunction of literals.  (We can also eliminate $x \neq f(y_1,\ldots,y_n)$ if needed.)
-Rewrite rule that describes this transformation:
-\[
-    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 =====
-Consider a formula in flat form.  Let language ${\cal L}$ contain only the symbols occurring in the formula.  For the fixed set of variables occurring there is a finite number of flat atomic formulas.
-Assume $K$ variables. ($K = |FV(C)|$)
-Number of $R(y_1,\ldots,y_n)$ is: $K^n$
-Number of $x=y$ atomic formulas is: $K^2$
-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.
-**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 =====
-For each flat literal $L$, $C$ is equivalent to $(C \land L) \lor (C \land \lnot L)$ and $\lnot L$ is a conjunction of flat literals.
-Let variables of $C$ be $V_C$.
-//Atomic diagram conjunction// is a flat form such that for each flat atomic formula $A$ in variables $V_C$ either $A$ or $\lnot A$ appears.
-Each conjunction of flat literals is equivalent to a disjunction of atomic diagram conjunctions.  Such form can be very large and we do not need to go that far, but we can when we need to.
-Note: if we simply guess all possible conjunctions of literals and negations, some of them will be unsatisfiable in the theory.  Those are useless and we should eliminate them.  For example, if we consider equality literals, then
-\[
-    x \neq z \land y = z \land x = y
-\]
-is unsatisfiable.  Only those conjunctions of equality literals can be satisfiable that correspond to an equivalence relations on variables.  Such conjunction of literals that corresponds to an equivalence relation is called **arrangement** in the context of combination techniques.
-$C$ can be rewritten as such (notating $L_i$ the $i^{th}$ flat literal and $A_{n+i}^{\alpha^{n+i}}$ the truth value of the $i^{th}$ variable):
-$C = \bigvee_{\alpha_{n+1}, ..., \alpha_m}L_1\land ...\land L_n\land A_{n+1}^{\alpha^{n+1}}\land ...\land A_m^{\alpha^m}$
-Which in turn can be rewritten as (notating $Ar_i$ the $i^{th}$ possible arrangement):
-$C \leadsto \bigvee_i C \land Ar_i$