about 4 years ago

本篇介紹如何用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.logicLogicParser

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

接著,在 nltk.sem.logic 中要用哪些符號,來表示邏輯運算符號
根據以下結果,就可以知道了
例如,要表示exists 符號,要用 exists 字串

>>> logic.boolean_ops()
negation         -
conjunction      &
disjunction      |
implication      ->
equivalence      <->
>>> logic.equality_preds()
equality         =
inequality       !=
>>> logic.binding_ops()
existential      exists
universal        all
lambda           \

然後,我們來看看如何輸入一階邏輯式的組成
一階邏輯式可以分為 FunctionArgument 兩部份
例如:

manwomanFunction ,而 Gary , xArgument

Argument 的部份,可以是 Constant 也可以是 Variable
例如 GaryConstant ,是已知的值,不能被代換成其他的值
xVariable ,是未知的值,可以被帶換成其他的值

把以上邏輯式子輸入進去

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

接著看看它們的 FunctionArgument

>>> e1.function
<ConstantExpression man>
>>> e2.function
<ConstantExpression woman>
>>> e1.argument
<ConstantExpression Gary>
>>> e2.argument
<IndividualVariableExpression x>

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

然後,輸入以上式子

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

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

3. Theorem Proving

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

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

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

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

結果為True, 表示的推導成立
但如果你執行prover9後顯示出這樣:

>>> 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的例子:

把前提和結論輸入

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

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

← Note on Xpath Parsing Python nltk -- Logic 2 : Lambda Calculus →
 
comments powered by Disqus