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

推理規則與歸結 
推理規則是構造有效推論的方案。這些方案建立在一組叫做前提的公式和叫做結論的斷言之間的語法關係。這些語法關係用於推理過程中，新的真的斷言從其他已知的斷言得出。在形式邏輯的設置中，推理規則通常用如下形式給出：

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

白話來說，就是"如果前提..成立，那麼結論..成立"。


歸結 (resolution)
歸結是對於命題邏輯和一階邏輯中的句子的推理規則，從兩個子句生成它們所蘊含的一個新的子句，可作為一種反證法的定理證明技術。

$\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}$

歸結規則生成的子句叫做兩個輸入子句的歸結(resolvent)。

肯定前件 (Modus ponens)

肯定前件是有效的、簡單的論證形式(常縮寫為MP)

肯定前件規則可以用相繼式符號寫為:

$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.__

矛盾歸結法 Resolution Refutation
當外加上完備的查找算法的時候，歸結規則生成一個可靠的和完備的算法來決定命題公式的可滿足性，並且經過擴展，決定句子在一組公理下的有效性。

這種歸結技術使用反證法，並基於在命題邏輯中的任何句子都能轉換成等價的合取範式句子的事實。步驟如下:

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)
在布爾邏輯中，一個公式是合取範式(CNF)的，如果它是子句的合取。作為規範形式，它在自動定理證明中有用。它類似於在電路理論中的規範和之積形式。在 CNF 公式中可以包含的命題連結詞是與、或和非。非運算元只能用做文字的一部分，這意味著它只能在命題變量前出現。

定義 : A wff is in Conjunctive Normal Form (CNF) if it is a conjunction of disjunctions:
$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.

例如 : 下列所有公式都是 CNF :

$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.


各別的CNF轉成規則庫中的clause(rule)
大括弧內是AND小括弧內是OR，由各別的CNF變成規則庫中的clause (rule規則庫中的clauses彼此都是Λ，如果CNF中有Λ，則一條 CNF可以被拆成多條clauses。

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

規則庫寫作Clause form好處是可做歸結(Resolution)。




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
Unification 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)) }
上例中 unifier 的表示法 : {a/w, b/x}

e.g.2
例如，對於多項式 $X2$ 和 $Y3$ 可以通過採納 $X = Z3$ 和 $Y = Z2$ 而同一(unify)到 $Z6$。

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}

最終目標 - The FOL Resolution Algorithm
學完了基本的Resolution Refutation、Prenex normal form、Skolem normal form(Skolemization)和 Unification，終於來到了最後一關，把這些東西串起來，集大成之 The FOL Resolution Algorithm!

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