# 訊息

## English

Included page "ai:booleanlogic" does not exist (create it now)

``````何謂 unification，可以括充到多值系統嗎 ?

Boolean Example:
A & -C     ;   B & C        A & B

A : {a1, a2}
B : {b1, b2, b3}
C : {c1, c2, c3}
a1 & b1 & c1  ; a1 & b1 & c2;  a1 & b1 & c3     a1 & b1

```
``````Chapter 4 : Boolean Logic

Proposition : 簡單的 theorem , 常識的定理 (forward reasoning)。
Lemma : 為證明此 theorem 所需的輔助定理（引理 backward reasoning）。
Theorem : 欲證明的定理。
Collary : 由此定理所導出來的有用的衍生定理。

Proof Theory
A set of axiom + A set of inference rule

Δ├ φ ( Δ deduce φ,   φ is a theorem of Δ)
if there is a sequence of boolean expressions (φ1, .., φn)  such that
(1) φn is φ
(2) for every i≦n, φi in Δ or φi is an axiom.

Soundness :
A proof theory is Sound if for every φ,├φ ==> ╞ φ

Completeness :
A proof theory is complete if for every φ,╞ φ==>├φ

To prove soundness need to prove :

1. Axiom are sound :
For every axiom φ, NIL=>φ

2. Inference are sound :
MP: if ╞ X and ╞ (X=>Y) then ╞ Y

Boolean Logic

Syntax :
Boolean variable X = {x1, x2,... , xn...}
logical connectiver : &, or, -, =>
Boolean expression (BE)
(1) Every variable is a BE
(2) If a, b is BE, so is a&b, a or b, -a, a=>b
(3) Nothing else is a BE
Semantic :
Truth assignment ==> T:X -> {T, F}
(1) Given T, Boolean expression φ, (T╞ φ)
(2) φ is a&b ==> T╞ a and T╞ b
(3) φ is -a ==> not T╞ a
(4) φ is a or b ==> T╞ a or T╞ b
(5) φ is a=>b ==> T╞ -a or T╞ b
(6) φ is ab ==> T╞ (a=>b) & T╞ (b=>a)

φ is satisfiable if there is a T s.t T╞ φ
φ is valid if T╞ φ for all T in which all variable assignment in φ
// If φ is valid we also call φ a tautology
φ is unsatisfiable if there is no T s.t. T╞ φ

Atom : a variable
Literal : an atom or it's negation
Clause : a disjunction of literals
Set of clauses : S = a conjunction of clauses S = {c1, c2, …, cn} = c1 & c2 & ... & cn

A propositional formula is in clausal form if it is represented as a set of clauses.

Every boolean formula can be expressed in clausal form.

To decide if φ is valid, both Davis-Patumn method and Ground resolution convert -φ into clausal form then try to prove that it is unsatisfiable.

Truth Table Proof Theory
φ is valid iff T╞ φ for the 2^n truth assignment in which validity the n variable of φ appear

Hilbert style proof theory : (logical induction system)
Axiom :
(1) a=>(a=>a)
(2) a=>(b=> a&b)
(3) a&b =>a
(4) a&b =>b
(5) a=> a or b
(6) b=> a or b
(7) (a or b) => ((a=>r)=>((a=>b)=>r))
(8) (a=>b) => ((a=>(b=>r))=>(a=>r))
(9) (a=>b) => ((a=>(-b))=>-r)
(10)--a=>b

Inference Rule :
Modus Ponens :
a, a=>b ==> b

Gentzen style proof theory (Sequent Calculus)
Axiom :
(1) T,φ ├ Δ,φ
(2) T∪{φ} ├ Δ∪{φ}

Inference Rule :

// "," 在左邊表示 &
// "," 在右邊表示 or
// ";" 表示兩式之 &
// 目的：不斷縮短算式的長度。

(&├)                         (├&)
T, a, b ├ Δ                   T ├ a, Δ ; T ├ b, Δ
-----------------------------   ----------------------------
T, a & b ├ Δ                       T ├  a & b, Δ

( or ├)                          (├ or )
T ├ Δ, a; T ├ Δ, b              T ├ Δ, a, b
-----------------------------   ----------------------------
T a or b├ Δ                  T ├ Δ, a or b

(-├)                             (├ -)
T ├ Δ, a                    T, a ├ Δ
-----------------------------   ----------------------------
T, -a ├ Δ                   T ├ Δ, -a

(=>├)                         (├ =>)
T ├ Δ,a; T, b ├ Δ              T, a ├ Δ, b
-----------------------------   ----------------------------
T, a=>b ├ Δ                    T ├  a=>b

(cut rule)
T, a => Δ; T => Δ, a
------------------------- + (cut elimination theorem) = complete.
T => Δ

Sequent : T=>Δ where T,Δ are finite sets of BE's
{φ1,...φn}=>{ci1, ...cim}
Informally we want to capture φ1,...,φn => ci1,...cim

Davis Patumn proof method :

Method : divide and conquer
S
----------------------------
P = true        ;    P = false
S[p = true]        S[p=false]

Case 1 : Unit clauses rule    :    S&{L}  S{Ltrue}
Case 2 : Elimination rule     :    S&{Ci|L}  S
Case 3 : Split rule        :    S  S[Ptrue] ; S[pfalse]

Theorem : S is unsatisfiable iff all sets producted for Davis Patumn are unsatisfiable.
φ = {(p|q) & (-q|s) & (-s|p) & (-p|r) & (-r|-p|t) }  (t & -r)
-φ = (p|q) & (-q|s) & (-s|p) & (-p|r) & (-r|-p|t) & (-t | r)

S
-------------------------------------------------
S[p=true]             ;         S[p=false]
{-q|s, r, -r|t, -t|r}        {q, -q|s, -s, -r | -t}
--------unit clause of r    ----------------unit clause of -s
{-q|s, t, -t}                {q, -q, -r|-t}
-------------                ----------------
false                    false

If there is a P s.t P, -P in S then S is unsatisfiable.

Ground Resolution Proof Theory

Methodology :

To prove that φ is valid, we prove that -φ is unsatisfiable instead.

Inference Rule :

c or x; d or -x
---------------
c or d

Example :

s = { p or q, -p or r, -r or -s or t, q or s, -q , -r or -t}

p or q -p or r
\     /
-r or -t    q or r    -r or -s or t
\  /      \    /
q or -t     q or -s or t
\    /
q or -s    q or s
\   /
q    -q
\   /
False

Completeness of ground resolution theorem :
φ is valid iff NIL can be deduced from S using ground resolution.
Proof :
Given a set of propositional variable {p1, ..., pn}
A semantic tree is
S
T        F            p1
T       F  T        F        p2
P3…

Each nodes represents is a partial interpretation of the variables assigned so far, where values are indicated as labeled as the edges.
If S is unsatisfiable,
S=c1&c2&...&cn
Then each ci is a false

A tree in which all pathes ends in a falsified node is called a closed semantic tree.

Proposition : If S is unsatisfiable then one can get a closed semantic tree no matter how the variable are ordered.
Proof of proposition
Choose the (longest) path from the closed semantic tree.

/
/ \
T          F
D|-P        C|P
Then ground resolution will produce C|D
By induction , ground resolution is complete.

Refinement 1 : Ordered ground resolution
(assumed there is an ordering on variable, any order is good)
If P is the longest atom assigning, C|P & D|-P  C|D

Refinement 2 : Positive ground resolution
(Choose the rightest path with all positive asignment)

Refinement 3 : positive ordered ground resolution
(Choose the all positive clause with longest path)

The Refinement doesn't means that the produced proof will be shorter than resolution.
It means that the choosing space of each step is small than the resolution case.

My Refinment : Shortest first ground resolution

My Refinment : Prune the other branch that is not needed any more.
P|-q     prune the -p&q

Boolean Ring :

normal form 來比較是否相等。
literal :
.      and
+      exclusive or
1      true
0      false
Axiom :
a set of rewrite rules which are used to perform reduction.
. + : commutative and associative.

x+y = y+x             x.y = y.x
(x+y)+z = x+(y+z)    (x.y).z = x.(y.z)
Inference Rule :
x or y  ==> x.y + x + y
x => y  ==> xy + x + 1
x = y   ==> x + y + 1
-x      ==> x + 1
x + 0   ==> x (identity)
x . 0   ==> 0 (zero)
x . 1   ==> x (unit)
x . x   ==> x (idempotent law)
x + x   ==> 0 (nilpotent law)
x + y   = y + x (communicative law)
x . y   = y . x
(x+y).z ==> xz + yz (distributive law)
(x + y)+ z = x + (y + z) (associative law)
(x . y) . z = x . (y . z)
monomial : product of distinct variables       xyz, z, 1
polynomial : sum of distinct monomials         xy + x + xyz = 1

Boolean ring normal form
Canonical rewrite system BR (Hsiang, 1982)
X | y     -> xy + x + y
X = y     -> x + y + 1
-x        -> x + 1
x => y    -> xy + x + 1
x + 0    -> x
x + x     -> 0
x . 1    -> x
x . 0    -> 0
x . x    -> x
x . (y+z)-> xy + xz

Claim :
Every Boolean expression has a unique boolean ring normal form which can be obtained through reduction. (Any Boolean formula can be uniquely translate into an equivalent BRNF.)
Example :
absorption law : p or (p&q) = p
ppq + p + pq ==> pq + p + pq ==> p + 0 ==> p
Proof :
If BRNF is not unique then
There are two BRNF (p1, p2) for some case
Such that p1+p2 = m1 + m2 + … =0
Let m1 be the shortest monomial in p1+p2,
Let all variable in m1 be 1, and the other variable be 0, then
p1+p2 (m1 = 1) = 1, contradiction   -><-
Method 2: counting argument
M1 + m2 + … + mk
There are 2n monomial for n variable expression,
So there are 2^2n    BRNF for n variable expression,
It can be 1-1 mapping to Boolean function.

Theorem：
valid                                            1
φ is { unsatisfiable             } if its BNF is { 0        }
satisfiable but not valid                    otherwise
Remark :
A BRNF is 0, 1 or m1+...+mr where each mi is a conjunction of boolean variable and the mi's are distinct from each other.

Inference mechanism :
reduction : given φ, reduce φ using BR until no any reduction can be done.

Boolean ring equations :
(x | y | -z) & (-x | -y | -z) & (y | -z | -t)
if we want to satisfy the equation above then
y | -z | -t = 1    De Morgan's law  -(y | -z | -t) = 0
so -y & z & t = 0 (Replace & by ., - by 1+)
(1+y) . z . t = 0 (expand the equation )
zt + yzt = 0
a expression x1 | x2 | .. | xn wan be rewrite to a BRNF with 2n-1 urinal ,
so operator | is expensive.

Simplification
F = (x | y) & (x | -y) & (-x | y) & (-x | -y)
Calculation :
Xy + x + y + 1 = 0        0 = 0 + 0 + 1 , contradiction -><- so F is unsatisfiable.
Xy + y = 0                0 + y = 0,     y = 0
Xy + x = 0                0 + x = 0,     x = 0
Xy = 0                    let xy = 0    ↑

Simplification is sound, however, not complete.
For example :     Xy = 1    Yz = 1    Xz = 0 can not be simplified.

Superposition (最小公倍式)
Example 1 :
Xy = 1        xyz = z        z = 0
Yz = 1        xyz = x        x = 0
Xz = 0        xyz = 0        0 = 0
Xx = x
Yy = y
Zz = z
Example 2 :
Xyz = z + 1        Xyzt = (z + 1) . t        xyz = t
Xyt = xy + zt        Xyzt = (xy + zt) . z        z = t + 1

M1 = m2                        m1m1'
M1' = m2'        m2(m1m1'/m1)        m2'(m1m1'/m1')

Simplification + superposition + idempotent law  complete
{x|y, -x|s, -y|t, -s|t, -t|s, -s|-t}
xy = x + y + 1
xs = x
yt = t
st = s
st = t
st = 0

Davis-Putnum in Boolean ring
Variety     -- number of different variable in an equation.
Degree    -- length of the largest nominal in an equation
Length    -- (distinct monomials) in an equation
Eample :    Xyz + zy + ut + 1        variety = 5, degree = 3, length = 4

Linear : degree <= 1
X+y+z = 1, x+1 = 0, 1 = 0, …

Binomial : length <= 2
Xyz + xu = 0, xy + t = 0, …
Xy + x + y = 0, x+y+1 = 0, x+1 = 0,…

Theorem
Linear equation can be solved in time O(n3) (by Gaussian Elimination)
Binomial equation can be solved in linear time. ( = HORN-SAT)
Quadratic equations can be solved in linear time. (= 2-SAT)

A reasoning model of Binomal-Linear
Binomial equations        B  optimize
Linear equations            L  optimize   ↑ lift
Unit equations            U

Important : All Boolean function  can transform into the linear + binomial + unit equation by adding variable.

Inference rules
1.    Tautology Deletion
S'{0=0} => S'        S'{1=1} => S'
1 = 0 => unsatisfiable
2.    Decomposition
B'{x1'.x2'…xm'}  1} => B'{x1'->1, x2'->1, …,xm'->1}
3.    Simplification
Perform only with B or L, but not across them.
4.    Unit Rule :
Collect all equations x=0 or x=1 into U, Use U to simplify B, L.
5.    Splitting Rule :
U => U{X1} ;  U{X0}
6.    Transportation
Given y1+y2+…+yk-1+yk = 0, where c in {0, 1}
Add y1y2..yk = y1y2..yk-1 . c            to B when K is odd.
Add y1y2..yk = y1y2..yk-1 . (c+1)     to B when K is even.
Example
X+y = 1        =>    xy = 0
X+y = 0        =>    xy = x
X+y+z = 1    =>    xyz = xy, xyz = xz, xyz = yz
X+y+z = 0    =>    xyz = 0

Discovering essential rules by local search
V : the set of variables
A : assignment on V
For all X in V , either x = 0 in A or x = 1 in A, but not both
P : partial assignment,  subset of A
 : Complete fence
the set of partial assignments, such that given any (full) assignment A on V, P in  with
P is subset of A
f(x1,x2..,xm) : Schema
Example : if f(x,y) = x+xy then f(x,y) = {x+xy, y+yx}
fr(P) : the set of unit literals that can be inferred in (B; L; U) without the Splitting Rule.
1.    Predetermine a set of schemata F.
2.    Choose a complete fence 
3.    For each P in , evaluate fr(P)
4.    W in V , with for any x in W, either x = 0 in fr(P) or x = 1 in fr(P) for all P in .
5.    Bind W with f in F
Find instances of f that output the same value for all p in 

P1        P2    ...    Pm
Fr(P1) fr(P2)...    fr(Pm)
W
↓
F
Ex : F = {x+y, xy, xy+x, x}
Let F(x1, …, xm) and F'(x1', …, xm') be different formulations of the same boolean function
(with xi  xi')
Then F  F' can be proved
Example：
X1 : x+y,     x1': (x|y)&(-x|-y)
X2 : 1+z+t    x2': (z|-t)&(-z|t)
F(x1,x2) = x1+x2
F'(x1',x2') = (x1'|x2') & (-x1'|-x2')
To prove
(X+y) + (1+z+t)  (((x|y)&(-x|-y)) | ((z|-t)&(-z|t))) ^ (-((x|y)&(-x|-y)) | -((z|-t)&(-z|t)))

Ordered binary decision diagram (OBDD) (R. E. Bryant 1986)
1. graph based NF
2.    unique wrt the variable (node : CNF , DNF : no unique normal form, no variable sharing too)(BRNF : no variable sharing too)

Provide an efficient way to manipulate Boolean function
X    Y    Z    F    G    F&g    F|g    F=>g
0    0    0    0    0    0    0    1
0    0    1    1    1    1    1    1
0    1    0    1    1    1    1    1
1    0    0    1    0    0    1    0
0    1    1    0    1    0    1    1
1    0    1    0    0    0    0    1
1    1    0    0    1    0    1    1
1    1    1    1    1    1    1    1

Assume an ordering on variable
X1 < X2 < ... < Xn

X1X2X3' + X1X2X3

X1                   X1             X1
1/   \                / \            /  |
X2   X2              X2 X2          X2 |
1/ \   / \       =>   /\  /\    =>  / \ |
X3  X3 X3 X3         1 0  0 0      1    0
/ \ / \ /\ / \
1  1 0 0 00 0 0

Idea : using Shannon entropy

φ : Boolean expression
φ = φ(x=1)*X + φ(x=0)*X'

transform φ into its BDD give order X1<...<Xn

Expansion X             Share

t ==> X          t1==>X   X<==t2           X
/ \               |\ /|        =>      / \
φ(X=1) φ(X=0)        |/ \|               ts  tu
ts   tu

Delete                          Merge

t1==>X          t1==>t2      t1 t2     t1 t2
| | ==>                   |   |      \ /
t2                       t3 t3       t3

Theorem : OBDD is unique for any given φ and order.

2SAT in P
A clause is definite iff it has exactly one positive literal.
A clause is Horn iff it has at most one positive literal

HORNSAT :

HORNSAT in P (3SAT is NP complete)

HORN = DEF + NEG
example : (-x|-y|-z|-w|u)&(-x|-y|z)&(-z|-w|v)&(-x|-z|w)
&(-x|-y)&(-x|-z|-u) & x & y

We consider a truth assignment T as a set that contain all variable assigned value true.

HORN-ASSIGN(φ) returns T
T := empty
loop
Pick one unsatisfied x1&…&xn => y from Def
T := T ∪ {y}
until all clauses in Def are satisfied
end

Example : (in HORN example above)
{x, y, z, w, v, u} will added into T in sequence.

Claim 1 : The T produced satisfy all implication in φ
Claim 2 : If there is a T’ that satisfies all implication in φ then T in T’
Proof :
Let y be the first variable in T\T’ then
there is a clause x1&..&xn => y s.t.
x1,..,xn in T ∩ T’, so T’ !╞  (x1&..&xn=>y) -><-

Claim 3 : φ is satisfiable iff T╞ φ
Proof :
<= trivial
if T!╞φ then there is a claim -x1&..&-xn in φ
s.    t. T!╞-x1|..|-xn
ie : {x1,..,Xn} in T
If T’╞φ by claim 2 (T in T’)
then T!╞{-x1,..,-xn}

Every set of boolean formula can be express as a set of clauses, each of which has almost 2 positive literal.

A|B|C|-D  (A|B|-T)(T|C|-D)

Under HORN : classical logic and intuitionistic logic are the same.
Classic Logic : law of excluded middle  p|-p = true
Intuitionistic logic : No law of excluded middle.

Example :
P(x,0,x)
P(x,y,z)P(x,s(y),s(z))

Proof 1 : Exist z, P(5, 3, z)
P(x,0,x)       -P(x,y,z) | p(x,s(y),s(z)),      -P(5,3,z)
-P(5,2,z-1)
-P(5,1,z-2)
P(x, 0, x) bind  -P(5,0,z-3)  // z-3 = 5
NIL (z-2=6, z-1=7, z=8)
// The resolution above is what we called input resolution
Input Resolution  backward reasoning
In every resolution steps, one of the clauses must be an input clause.

Proof 2 : Exist z, P(5, 3, z)
P(x,0,x)       -P(x,y,z) | p(x,s(y),s(z))
P(x,s(0),s(x))
P(x,2,x+2)
P(x, 3, x+3) bind P(5, 3, z) // x = 5, z = x+3 = 8

// The resolution above is what we called unit resolution
Unit Resolution  forward reasoning
In every resolution steps, one of the clauses must be a unit clauses.

Theorem : In HORN logic, both unit and input resolution are complete.
(Remark : not true in First Order Logic)```
```