Some formulas and some linearizations.

Here is some examples of how a formula looks like before and after linearization. Let us consider again F1, F2, ... .

In[28]:=

F1 Lin[F1]

Out[28]=

Impl[Conj[Disj[Neg[A], C], B], ]

Out[29]=

(((¬A∨C)∧B))

In[30]:=

F2 Lin[F2]

Out[30]=

Un[x, Impl[Conj[Disj[Neg[A], C], B], ]]

Out[31]=

∀x.(((¬A∨C)∧B))

In[32]:=

F3 Lin[F3]

Out[32]=

Ex[x, Impl[Conj[Disj[Neg[A], C], B], ]]

Out[33]=

∃x.(((¬A∨C)∧B))

In[34]:=

F4 Lin[F4]

Out[34]=

Impl[Ex[x, Un[y, f(x)≤f(y)]], Ex[x, Conj[f(x)≤f(g(x)), f(x)≤f(h(x))]]]

Out[35]=

(∃x.∀y.f(x)≤f(y)∃x.(f(x)≤f(g(x))∧f(x)≤f(h(x))))

In[36]:=

F5 Lin[F5]

Out[36]=

Un[x, Neg[Neg[Disj[Ex[y, P(x,y)], Neg[Ex[y, P(x,y)]]]]]]

Out[37]=

∀x.¬¬(∃y.P(x,y)∨¬∃y.P(x,y))

In[38]:=

F6 Lin[F6]

Out[38]=

Ex[x, Un[y, f(x)≤f(y)]]

Out[39]=

∃x.∀y.f(x)≤f(y)

In[40]:=

F7 Lin[F7]

Out[40]=

Un[x, Disj[Ex[y, Un[z, P(x,y,z)]], Un[y, Ex[z, Neg[P(x,y,z)]]]]]

Out[41]=

∀x.(∃y.∀z.P(x,y,z)∨∀y.∃z.¬P(x,y,z))

In[42]:=

F8 Lin[F8]

Out[42]=

Un[x, Un[y, Impl[x<y, Ex[z, Conj[x<z, z<y]]]]]

Out[43]=

∀x.∀y.(x<y∃z.(x<z∧z<y))

In[44]:=

F9 Lin[F9]

Out[44]=

Ex[x, Ex[y, Conj[Conj[x<y, f(x)≤f(y)], Ex[z, Conj[y<z, f(y)≤f(z)]]]]]

Out[45]=

∃x.∃y.((x<y∧f(x)≤f(y))∧∃z.(y<z∧f(y)≤f(z)))


Created by Mathematica  (October 17, 2006)