## AI - Ch12 邏輯(5), 歸結論證 Resolution-refutation proofs

前提#1
前提#2
...
前提#n
結論

$\frac{a_1 \lor \ldots \vee a_{i-1} \vee a_i \vee a_{i+1} \vee \ldots \lor a_n, \quad b_1 \lor \ldots \vee b_{j-1} \vee b_j \vee b_{j+1} \vee \ldots \lor b_m} {a_1 \lor \ldots \lor a_{i-1} \lor a_{i+1} \lor \ldots \lor a_n \lor b_1 \lor \ldots \lor b_{j-1} \lor b_{j+1} \lor \ldots \lor b_m}$

$P \to Q, P \vdash Q$

$\qquad\frac{P \rightarrow Q, P}{Q}$

[例題] modus ponens
Let a, b, c be 3 propositions. Assume a knowledge base, KB, includes a∨b, a→c, b→c.
• Does KB entail c? __Yes__
• By applying modus ponens, is it possible to derive c? __No__
• Modus ponens is sound because (i or ii) __whatever it can prove is correct.__

1.   在知識庫中所有句子和「要證明的句子的否定」都合取連結。

$(A_1) \wedge (A_2) \wedge ... \wedge \neg(要證明的句子)$

2.   應用歸結規則直到
• 推導出空子句：則全部的公式是不可滿足的(或者說矛盾的)，所以最初的猜測是從這些公理中推出的結論
• 不能推導出空子句：不能應用歸結規則推導更多的新子句，則這個猜測不是最初的知識庫的定理

[例題1] Propositional Resolution

[例題2] Any conclusion follows from a contradiction

[例題3] Refutation Proofs in Tree Form

[例題4]
Model the following problem in normal clausal form, using the predicates:
$circles(X,Y), planet(X), moon_of(X,Y).$

a.  Jupiter is a planet.           $planet(Jupiter)$
b.  IO is a moon of Jupiter.  $moonof(IO, Jupiter)$

c.  Planets circle the sun.
(沒用be動詞時會有"->"：如果是Planets時，則circle the sun.)
$planet(X) -> circles(X,Sun)$
$¬planet(X) ∨ circles(X,Sun)$

d.  A moon circles its planet.
$planet(Y) moonof(X,Y) -> circles(X,Y)$
$= ¬(planet(Y) \wedge moonof(X,Y)) ∨ circles(X,Y)$
$= ¬planet(Y) ∨ ¬moonof(X,Y) ∨ circles(X,Y)$

e.  If object_1 circles object_2, and object_2 circles object_3, then object_1 circles object_3.
$circles(ob1,ob2) \wedge circles(ob2,ob3) -> circles(ob1,ob3)$
$= ¬( circles(ob1,ob2) \wedge circles(ob2,ob3) ) ∨ circles(ob1,ob3)$
$= ¬circles(ob1,ob2) ∨ ¬circles(ob2,ob3) ∨ circles(ob1,ob3)$

Prove that IO circles the sun by resolution.
¬(goal):  g. $¬circles(IO,Sun)$
a+c      :  h. $circles(Jupiter,Sun)$
a+b+d :  i. $circles(IO,Jupiter)$
h+i+e   :  j. $circles(IO,Sun)$
g+j        :  {}, $PROVE$

Propositional  Resolution - 合取範式 (Conjunctive Normal Form, CNF)

$A_1 Λ A_2 Λ A_3 Λ ... Λ A_n$ where each clause, $A_i$, is of the form : $B_1 v B_2 v B_3 v...v B_n$ The B’s are literals.

$A \wedge B$
$\neg A \wedge (B \vee C)$
$(A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)$
$(\neg B \vee C)$

[感覺] CNF也就是數位電路所稱的 "Product of Sums"

WFF converting to CNF
Any wff can be converted to CNF by using the following equivalences.

Importantly, this can be converted into an algorithm – this will be useful when when we come to automating resolution.

In CNF is: (A V C) Λ (¬B V C) ;
In clause form, we write: {(A, C), (¬B, C)} ;

FOL Resolution (1) - 前束範式 Prenex normal form
A First-Order Predicate Calculus (FOPC, First-Order Logic) expression can be put in prenex normal form by converting it to CNF, with the quantifiers moved to the front.Every formula of first-order logic can be converted to an equivalent formula in prenex normal form.

A formula of first-order logic is in prenex normal form if it is of the form
$Q_1x_1...Q_nx_nM,$
where each Q_i is a quantifier $\forall$ or $\exists$ and M is quantifier-free.

For example, the formula
$\exists x \forall y \exists z(P(x) v Q(x,y,z))$
is in prenex normal form, whereas formula
$\exists x \forall y(P(x) v \exists zQ(x,y,z))$
is not, where  v  denotes OR.

FOL Resolution (2) - 斯科倫範式 Skolem normal form, Skolemization
A formula of first-order logic is in Skolem normal form if it is in prenex normal form with only universal first-order quantifiers.
$(∀ x_1)(∀ x_2)...(∀ x_n)M(W_1,...,W_k,x_1,...,x_n,f(W_1,...,W_k,x_1,...,x_n))$
• Every first-order formula may be converted into Skolem normal form while not changing its satisfiability via a process called Skolemization
• The resulting formula is not necessarily equivalent to the original one, but is equisatisfiable with it: it is satisfiable if and only if the original one is satisfiable.

Skolemization
1. Variables that are existentially quantified are replaced by a constant: ∃(x) P(x)
2. is converted to : P(c)
3. c must not already exist in the expression.

Skolem functions
If the existentially quantified variable is within the scope of a universally quantified variable, it must be replaced by a skolem function, which is a function of the universally quantified variable.

e.g.  (∀x)(∃y)(P(x,y)) 轉成 (∀x)(P(x,f(x)) ，例如 (∀x)(Love(x,lover(x))

[例題1]
$\exists x \forall y R(x,y) \Rightarrow\forall y R(a,y)$ 其中$a$為常數
$\forall x \exists y R(x,y) \Leftrightarrow\forall x R(x,f(x))$
$\forall x \forall y \exists z R(x,y,z) \Leftrightarrow\forall x \forall y R(x,y,f(x,y))$

[例題2]
1.    ∃(y) GoodMan(y) 轉成 GoodMan(c)
2.    存在某人去刺殺暴君,被刺殺則死亡 { ∃(x) kill(x, Caesar), ∀(y,z) kill(y,z) -> die(z) }
• Q : 暴君死亡了嗎? 或者 { ∃(x) kill(x, Caesar), ∀(z) ∃(y) kill(y,z) -> die(z) }
• A : 死了(依代換過程,是那個 “刺殺暴君的人”殺的){ kill(killer(Caesar), Caesar), ...}

Unification
Uniﬁcation is a basic operation on terms.  Two terms unify if substitutions can be made for any variables in the terms so that the terms are made identical.  If no such substitution exists, then the terms do not unify.

e.g.1
{ (P(w,x)), (-P(a,b)) } 替代後變成 { (P(a,b)), (-P(a,b)) }

e.g.2

e.g.3
X = 7                is true with X instantiated to 7
X = Y                is true with X aliased to Y (or vice versa)
foo(X) = foo(7)      is true with X instantiated to 7
foo(X,Y) = foo(3,4)  is true with X instantiated to 3 and Y to 4
foo(X,4) = foo(3,Y)  is true with X instantiated to 3 and Y to 4
foo(X) = foo(Y)      is true with X aliased to Y (or vice versa)
foo(X,X) = foo(3,4)  is false because there is no possible value for X
foo(X,4) = foo(3,X)  is false because there is no possible value for X

Most general unifier (mgu)
• MGU簡言之，是規則庫中大家都用得上的替代。
• A unifier (u) is a most general unifier (mgu) if any other unifier can be formed by the composition of u with some other unifier.
• An algorithm can be generated which obtains a most general unifier for any set of clauses.

[例題] most general unifiers

For each of the following pairs of sentences, give the most general unifiers,
or write "NONE" if none exists.
• P(A,B,C), P(x,y,z)
mgu : {x/A, y/B, z/C}
• Q(y,G(A,B)), Q(G(x,x), y)
mgu : {x/None , y/None}
• Older(Father(y), y), Older(Father(x), John)
mgu : {x/John, y/John)
• Knows(Father(y), y), Knows(x, x)
mgu : {x/None}

1.  First, negate the conclusion and add it to the list of assumptions.
(Using idea : Resolution Refutation)

2 .  Now convert the assumptions into Prenex Normal Form
• Eliminate arrows
• Drive in negation
• Rename (Standardize) variables apart
...
(Using idea : Prenex Normal Form)

3.  Next, skolemize the resulting expression
• Substitute a new name (constant) for each existential variable
• Substitute a new function for each universal variable in outer scopes
(Using idea : Skolem normal form (Skolemization) )

4.  Now convert the expression into a set of clauses
• Drop universal quantifiers
• Distribute ∨ over ∧, return clauses

5.  Now resolve the clauses using suitable unifiers.
(Using idea : Unification )

This algorithm means we can write programs that automatically prove theorems using resolution!

[用心去感覺] FOL 之中 變數的 (∀x), (∃x) 概念及處理方式
• 對於 (∀x) ... 我們略去，因為規則庫都是通則，其中變數x須在 Resolution 過程之中進行代換。
• 對於 (∃x) ... Before resolution can be applied, ∃ must be removed, using skolemization.

[例題] John有沒有他所愛的人?

[整合] Problem Solving

References

Chapter 8 Inference and Resolution for Problem Solving (非常好的教材!!)
http://www.iis.sinica.edu.tw/~jdwei/ai2011/PPT/AIchap08.pdf

wolfram.com - Prenex Normal Form
http://mathworld.wolfram.com/PrenexNormalForm.html

3.3  Unification and Logical Variables
http://www.eclipseclp.org/doc/tutorial/tutorial015.html

Wiki - Unification
https://en.wikipedia.org/wiki/Unification_(computer_science)

Wiki - 斯科倫範式
https://zh.wikipedia.org/wiki/%E6%96%AF%E7%A7%91%E4%BC%A6%E8%8C%83%E5%BC%8F

Wiki - 前束範式
https://zh.wikipedia.org/wiki/%E5%89%8D%E6%9D%9F%E8%8C%83%E5%BC%8F