訊息

English

P | -P => true // P 或 -P 中必然有一者為真。

人工智慧版

``````Chapter 6 : Agent that reason logically

Syntax   :
Describes the possible configurations that can constitute sentences.

Semantic :
Determines the facts in the world to which the sentences refer.
interpretation for syntax

Proof theory :
A set of axiom + a set of inference rule.

Proper reasoning should ensure that the new configurations represent facts that actually follow from the facts that the old configurations represent.

╞ (entail)   (proof by truth table)

KB ╞ φ  means for all case -KB|φ is always true

├ (derive)   (proof by axiom and inference rule)

KB ├ φ means that we can derive φ from KB by axiom and inference rule.
i

Sound : An inference procedure i that generates only entailed sentences is called sound or truth-preserving.
!├ φ & -φ

Proof : The record of operation of a sound inference procedure is called a proof (proof theory).

1. KB + {φ1...φi-1} => φi ( φn = φ )
2. For every i≦n φi in KB or φi is an axiom.

Complete : An inference procedure is complete if it can find a proof for any sentence that is entailed.
if φ is valid then ├ φ

(Natural language have evolved more to meet the need of communication rather than representation.)

Shapir-Whorf hypothesis :
the language we speak profoundly influences the way in which we think and make decision.

entail
Sentences ----------->  Sentence
↓                   ↓
Facts     ----------->  Fact
(理論與世界同構)

Valid sentence : (tautologies , analytic sentences)
A sentence that is true under all possible interpretations in all possible
worlds.

Satisfiable sentence :
there is some interpretation in some world for which it is true.
PL  : propositional logic
FOL : First Order Logic
TL  : temporal logic
PT  : probability theory
FL  : Fuzzy logic

Ontological Commitment    Epistemological Commitment
(What exist in the world)  (What an agent believes about facts)
PL   = (&,|,-) + proposition      true/false/unknown
FOL  = (&,|,-) + proposition
+ function + predicate     true/false/unknown
TL   = (&,|,-) + proposition
+ function + predicate
+ times                    true/false/unknown
PT   = proposition                degree of belief 0..1
FL   = degree of truth            degree of belief 0..1

Model : any world in which a sentence is true under a particular interpretation is called a model of the sentence under that interpretation.

A sentence φ is entailed by a KB if the models of KB are all models of φ.
ie : KB ╞ φ ==> ╞ KB=>φ, ie: KB=>φ is valid.

Prepositional logic :
Syntax :
1. A set of proportion {A, B, C,...} in this language
2. All form of P&Q, P|Q, -P (P=>Q) in this language
3. No other things is in this language
Semantic :
1. P => {T, F}
2. P    Q       -P      P&Q     P|Q     P=>Q
F    F       T       F       F       T
F    T       T       F       T       T
T    F       F       F       T       F
T    T       F       T       T       T
A sentence is valid if it's true in all row of truth table.
Proof Theory
Inference rule :
Modus ponens            : A=>B, A     --> B
And Elimination        : A1&A2...&An --> Ai
And Introduction       : A1,A2,...An --> A1&A2...&An
OR Introduction        : Ai          --> A1|A2...|An
Double Negation        : --A         --> A
Unit Resolution        : A|B, -B     --> A
Resolution              : A|B, -B|C   --> A|C
implication form    : -A=>B, B=>C --> -A=>C

Complexity of prepositional inference :
SAT problem in set NP-complete
Horn sentence : P1&P2...&Pn=>Q
HORN-SAT in set P

Monotonically :
if KB1╞A then (KB1 ∪ KB2)╞A```
```

計算理論版

``````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)```
```