Mark Chang's Blog

Machine Learning, Deep Learning and Python

NLTK Logic 1 : First Order Logic and Semantics

本篇介紹如何用python nltk 的應用,邏輯語意與推理

1. Introduction

邏輯語意學(logic semantics/formal semantics)

是早期的自然語言處理方法之一

因為自然語言中存在著某種邏輯成份

故可以用數理邏輯的公式來描述自然語言

進行各種邏輯推理

例如 Socrates is a man. 這句話,用一階邏輯式表示:

如果 Socrates is a man. 這句話為真,則:

另一個例子,如 All man are mortal 這句話,牽涉到 All 這個概念,用一階邏輯式表示:

接著,可以來用演繹法(Deductive Reasoning)進行推論

根據 Socrates is a man. 和 All man are mortal 這兩句話

可以推論出 Socrates is mortal

2. First-order Logic Expression

2.1 Logic Symbol

接著來實作logic inference,

首先,載入模組 nltk.sem.logic 和 LogicParser

1
2

>>> import nltk.sem.logic as logic
>>> lgp = logic.LogicParser()

接著,在 nltk.sem.logic 中要用哪些符號,來表示邏輯運算符號

根據以下結果,就可以知道了

例如,要表示exists 符號,要用 exists 字串

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

>>> logic.boolean_ops()
negation       	-
conjunction    	&
disjunction    	|
implication    	->
equivalence    	<->

>>> logic.equality_preds()
equality       	=
inequality     	!=

>>> logic.binding_ops()
existential    	exists
universal      	all
lambda         	\

然後,我們來看看如何輸入一階邏輯式的組成

一階邏輯式可以分為 Function 和 Argument 兩部份

例如：

man 和 woman 是 Function ,而 Gary , x 是 Argument

而 Argument 的部份,可以是 Constant 也可以是 Variable

例如 Gary 是 Constant ,是已知的值,不能被代換成其他的值

而 x 是 Variable ,是未知的值,可以被帶換成其他的值

把以上邏輯式子輸入進去

1
2
3
4
5
6
7

>>> e1 = lgp.parse('man(Gary)')
>>> e2 = lgp.parse('woman(x)')
>>> print e1
man(Gary)

>>> print e2
woman(x)

接著看看它們的 Function 和 Argument 

1
2
3
4
5
6
7
8
9
10
11

>>> e1.function
<ConstantExpression man>

>>> e2.function
<ConstantExpression woman>

>>> e1.argument
<ConstantExpression Gary>

>>> e2.argument
<IndividualVariableExpression x>

一階邏輯式子中也可以有 quantifier 的組成,例如 是 quantifier

然後,輸入以上式子

1
2
3

>>> e3 = lgp.parse('all y.(man(y) -> -woman(y))')
>>> print e3
all y.(man(y) -> -woman(y))

學會了以上這些,就可以輸入各種邏輯符號到nltk裡了

3. Theorem Proving

現在來看看怎麼用nltk做以下推理

首先,把前提和結論,由parser輸入

1
2
3

>>> p1 = lgp.parse('man(Socrates)')
>>> p2 = lgp.parse('all x.(man(x) -> mortal(x))')
>>> c  = lgp.parse('mortal(Socrates)')

接著要用Theorem Prover來證明這個推導成立

Theorem Prover是一種SAT solver

只要給定一些邏輯式

它就可以判斷這些邏輯式之間可不可以被滿足,有沒有矛盾

在nltk有提供很多種Theorem Prover的界面

例如Prover9, TableauProver, and ResolutionProver

但是只有提供界面而已,prover的核心程式還是要自己去下載

在這篇,我選用的是Prover9(其實用哪一種都可以）

首先,我們要先到此下載prover9, http://www.cs.unm.edu/~mccune/prover9/

下載好之後,請看compile的方法http://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/

compile好以後, 丟到 /usr/local/bin 目錄底下

（由於我都只用Linux或Mac系統,如果你使用Windows的話,我無法告訴你怎麼安裝,真抱歉）

接著我們用nltk的界面來呼叫prover9

1
2
3

>>> from nltk import Prover9
>>> Prover9().prove(c, [p1,p2])
True

結果為True, 表示的推導成立

但如果你執行prover9後顯示出這樣：

1
2

>>> Prover9().prove(c, [p1,p2])
which: no prover9 in (/usr/lib/jvm/java-1.7.0/bin:/usr/local/eclipse:/opt/ant/bin:/usr/lib64/qt-3.3/bin:/usr/local/maven/bin:/usr/local/bin:/bin:/usr/bin:/usr/local/sbin:/usr/sbin:/sbin:/usr/local/android-sdk-linux:......

這是因為prover沒有放到指定的資料夾

來看一個推理結果為False的例子：

把前提和結論輸入

1
2
3
4
5

>>> e1 = lgp.parse('man(Gary)')
>>> e3 = lgp.parse('all y.(man(y) -> -woman(y))')
>>> c1= lgp.parse('woman(Gary)')
>>> Prover9().prove(c1, [e1,e3])
False

當然,如果把結論改為

則結果為True

1
2
3
4
5
6

>>> c2=c1.negate()
>>> print c2
-woman(Gary)

>>> Prover9().prove(c2, [e1,e3])
True

4.Further Reading

關於邏輯語意,可到這網站 http://www.coli.uni-saarland.de/projects/milca/courses/comsem/html/

或參考這本書 Blackburn & Bos’ Representation and Inference for Natural Language

還有更多關於nltk的邏輯推理 http://www.nltk.org/howto/inference.html

Comments