這一節，通過翻譯自然語言表達式為一階邏輯來表示它們的意思。

并不是所有的自然語言語義都可以用一階邏輯來表示。

句法

一階邏輯保留了所有命題邏輯的布爾運算符但是它增加了一些重要的新機制。

1、命題被分析成謂詞和參數。

一階邏輯的標準構造規則承認以下術語：獨立變量、獨立常量、帶不同數量的參數的謂詞

例如：

Angus walks可以被形式化為walk(angus)，Angus sees Bertie可以被形式化為see(angus, bertie)。我們稱walk為一元謂詞，see為二元謂詞。

原子謂詞如see(angus,bertie)在情況s中是真是假不是一個邏輯問題，而是要依賴于特定的估值。這個值是我們為常量see,angus,bertie選擇的值。所以，這些表達式被成為非邏輯常量。

相比：邏輯常量（如布爾運算符）在一階邏輯的每個模型中解釋總是相同的。

2、檢查一階邏輯表達式的語法結構，這樣做的通常方式是為表達式指定類型。

基本類型：e是實體類型，t是公式類型（有真值的表達式的類型）

這兩種類型，可以形成函數表達式的復雜類型。

例如：<e,T>是從實體到真值，即一元謂詞的表達式的類型。

可以調用LogicParser來進行類型檢查：

>>>tlp = nltk.LogicParser(type_check=True)
>>>parsed = tlp.parse('walk(angus)')
>>>parsed.argument
<ConstantExpression angus>
>>>parsed.argument.type
e
>>>parsed.function
<ConstantExpression walk>
>>>parsed.function.type
<e,?>

注意，沒有識別出walk的類型，因為他的類型是未知的，有可能在這個上下文中會出現別的類型，如：<e,e>或<e,<e,t>>，我們需要制定一個信號來解決這個問題：

>>>sig = {'walk': '<e, t>'}
>>>parsed = tlp.parse('walk(angus)', sig)
>>>parsed.function.type
<e,t>

3、在一階邏輯中，謂詞的參數也可以是獨立變量，如x,y,z。e類型的變量都是小寫。獨立變量類似與人稱代詞，如he、she和it，其中我們為了弄清楚它們的含義需要知道它們使用的上下文。

例如：

(14) He disappeared.
(15) a. Cyrilis Angus’s dog.
b.Cyrildis appeared.
#可以看出來，14與15b是等價的。

he與Cyril的指稱相同。

同樣，也存在公指關系不同的關系。例如下面的句子，16a就指代不明。

(16) a. Angus had a dog but he disappeared.
b.Angus had a dog but a dog disappeared.

在看下面這個例子：

(17) a. He is a dog and he disappeared.
b.dog(x) &disappear(x)

對應17a構造了一個開放公式（17b）。

通過在（17b）前面指定一個存在量詞?x(“存在某些x”) ，我們可以綁定這些變量。

18a. ?x.(dog(x)&disappear(x))
b.At least one entity is a dog and disappeared.
c.A dog disappeared.

下面是，18a在NLTK中的表示：

(19) exists x.(dog(x) &disappear(x))

除了存在量詞，還有全稱量詞?X（“對所有x”），如（20）所示。

(20) a. ?x.(dog(x) →disappear(x))
b.Everything has the property that if it is a dog,it disappears.
c.Every dog disappeared.

在NLTK中，這樣表示：

(21) all x.(dog(x) -> disappear(x))

在一般情況下，變量x在公式φ中出現是自由的，如果它在φ中沒有出現在allx或existsx范圍內。

相反，如果x在公式φ中是受限的，那么它在allx.φ和exists x.φ限制范圍內。如果公式中所有變量都是受限的，那么我們說這個公式是封閉的。

NLTK中的LogicParser的parse()方法返回Expression類的對象。每個示例expr都有free()方法，返回一個在expr中的自由變量的集合。

例如：

>>>lp =nltk.LogicParser()
>>>lp.parse('dog(cyril)').free()
set([])
>>>lp.parse('dog(x)').free()
set([Variable('x')])
>>>lp.parse('own(angus, cyril)').free()
set([])
>>>lp.parse('exists x.dog(x)').free()
set([])
>>>lp.parse('((some x.walk(x))-> sing(x))').free()
set([Variable('x')])
>>>lp.parse('exists x.own(y,x)').free()
set([Variable('y')])

一階定理證明

我們要證明的公式，就是證明目標。

可以使用Prover9來演示證明：

>>>NotFnS= lp.parse('-north_of(f, s)') 
>>>SnF= lp.parse('north_of(s, f)') 
>>>R= lp.parse('all x.all y.(north_of(x, y) -> -north_of(y, x))') 
>>>prover= nltk.Prover9() ④
>>>prover.prove(NotFnS,[SnF, R]) ⑤
True

>>>FnS= lp.parse('north_of(f, s)')
>>>prover.prove(FnS,[SnF, R])
False

一階邏輯語言總結

我們將采取約定：<en, t>是一種由n個類型為e的參數組成產生一個類型為t的表達式的謂詞的類型。在這種情況下，我們說n是謂詞的元數。

真值模型

給定一階邏輯語言L，L的模型M是一個<D,Val>對，其中D是一個非空集合，稱為模型的域，Val是一個函數，成為估值函數。

估值函數按照如下的方式從D中分配值給L的表達式：

1、對于L的每一個獨立常量c，Val(c)是D中的元素

2、對于每一個元數n>=0的謂詞符號P，Val(p)是從Dn到｛True,False｝的函數。（如果P的元數為0，則Val(P)是一個簡單的真值，P被認為是一個命題符號。）

如果P的元數是2，然后Val(P)將是一個從D的元素配對到{True,False}的函數。我們將在NLTK中建立的模型中采取更方便的替代品，其中Val(P)是一個配對的集合S，定義如下：

(23) S = {s| f(s) = True}這樣的f被稱為S的特征函數。

NLTK的語義關系可以用標準的集合論方法表示：作為元組的集合。

例如：

假設我們有一個域包括Bertie、Olive和Cyril，其中Bertie是男孩，Olive是女孩，而Cyril是小狗。為了方便記述，我們用b、o和c作為模型中相應的標簽。我們可以聲明域如下：

>>>dom =set(['b', 'o', 'c'])

>>>v= """
... bertie =>b
... olive =>o
... cyril =>c
... boy=>{b}
... girl =>{o}
... dog=>{c}
... walk=>{o, c}
... see =>{(b,o),(c, b),(o, c)}
... """
>>>val = nltk.parse_valuation(v)
>>>print val
{'bertie':'b',
'boy': set([('b',)]),
'cyril': 'c',
'dog': set([('c',)]),
'girl': set([('o',)]),
'olive': 'o',
'see': set([('o', 'c'), ('c', 'b'), ('b', 'o')]),
'walk': set([('c',), ('o',)])}

一個形式為P(T1,... Tn)的謂詞，其中P是n元的，為真的條件是對應于(T1, ... Tn)的值的元組屬于P的值的元組的集合。

>>>('o', 'c') in val['see']
True
>>>('b',) in val['boy']
True

獨立變量和賦值

在我們的模型，上下文的使用對應的是為變量賦值。這是一個從獨立變量到域中實體的映射。

賦值使用構造函數Assignment，它也以論述的模型的域為參數。

>>>g= nltk.Assignment(dom, [('x', 'o'), ('y', 'c')])
>>>g
{'y': 'c', 'x': 'o'}

還可以查看賦值：

>>>print g
g[c/y][o/x]

下面演示，如何為一階邏輯的原子公式估值。

首先創建了一個模型，然后調用evaluate()方法來計算真值。

>>>m=nltk.Model(dom, val)
>>>m.evaluate('see(olive,y)',g)
True

當解釋函數遇到變量y的時候，不是檢查val中的值，而是在變量賦值的g中查詢這變量的值。

如果最終顯示為true，我們就說賦值g滿足公式see(olive,y)。

purge()函數可以幫助我們清楚綁定：

>>>g.purge()
>>>g
{}

確定模型中公式的真假的一般過程成為模型檢查。

量化

exists x.(girl(x) &walk(x))

#我們想知道dom中是否有某個u使g[u/x]滿足開放的公式(25)。
(25) girl(x) &walk(x)
思考下面的：
>>>m.evaluate('existsx.(girl(x) &walk(x))',g)
True

NLTK中提供了一個有用的工具：satisfiers()方法。它返回滿足開放公式的所有個體的集合。該方法的參數是一個已分析的公式、一個變量和一個賦值。下面是幾個例子：

>>>fmla1 = lp.parse('girl(x) | boy(x)')
>>>m.satisfiers(fmla1,'x', g)
set(['b', 'o'])
>>>fmla2 = lp.parse('girl(x) -> walk(x)')
>>>m.satisfiers(fmla2,'x', g)
set(['c', 'b', 'o'])
>>>fmla3 = lp.parse('walk(x) -> girl(x)')
>>>m.satisfiers(fmla3,'x', g)
set(['b', 'o'])

為什么fmla2是那樣的值，需要我們注意：->的真值條件意思是：fmla2等價于-girl(x)| walk(x)。

量詞范圍歧義

當我們給一個句子的形式化表示兩個量詞時：

(26) Everybody admires someone.

#（至少）有兩種表示形式
a. all x.(person(x)-> exists y.(person(y)&admire(x,y)))
b.exists y.(person(y)&all x.(person(x)-> admire(x,y)))

這兩個我們都可以使用，但是這兩個的含義是不一樣的：27b邏輯上強于27a。

我們使用術語量化范圍來區分兩個邏輯：

?的范圍比?廣，而在（27b）中范圍順序顛倒了，所以現在我們有兩種方式表示（26）的意思，它們都相當合理。換句話說，我們稱（26）關于量詞范圍有歧義，（27）中的公式給我們一種使這兩個讀法明確的方法。然而，我們不只是對與（26）相關聯的兩個不同的表示感興趣；我們也想要顯示模型中的兩種表述是如何導致不同的真值條件的細節。

為了更仔細的檢查歧義，讓我們對估值做如下修正：

>>>v2= """
... bruce =>b
... cyril =>c
... elspeth =>e
... julia =>j
... matthew=>m
... person=>{b,e, j, m}
... admire =>{(j, b),(b, b),(m, e), (e, m),(c, a)}
... """
>>>val2 = nltk.parse_valuation(v2)

在這個模型中，公式（27a）為真而（27b）為假。

探索這些結果的方法之一是使用Model對象的satisfiers()的方法。

>>>dom2 =val2.domain
>>>m2=nltk.Model(dom2, val2)
>>>g2= nltk.Assignment(dom2)
>>>fmla4 = lp.parse('(person(x) -> exists y.(person(y)&admire(x, y)))')
>>>m2.satisfiers(fmla4,'x', g2)
set(['a', 'c', 'b', 'e', 'j', 'm'])
#這表明fmla4 包含域中每一個個體。相反，思考下面的公式fmla5；沒有滿足y的值。
>>>fmla5 = lp.parse('(person(y) &all x.(person(x)-> admire(x, y)))')
>>>m2.satisfiers(fmla5,'y', g2)
set([])
#也就是說，沒有大家都欽佩的人。看看另一個開放的公式fmla6，我們可以驗證有一
#個人，即Bruce，它被Julia和Bruce都欽佩。
>>>fmla6 =lp.parse('(person(y) &all x.((x =bruce | x = julia) -> admire(x, y)))')
>>>m2.satisfiers(fmla6,'y', g2)
set(['b'])

模型的建立

模型的建立，是給定一些句子的集合，嘗試創造一種新的模型。如果成功，我們就會知道集合是一致的，因為我們有模型作為證據。

Mace4(Mace4 searches for finite models and counterexamples.)

>>>a3 = lp.parse('exists x.(man(x)&walks(x))')
>>>c1 = lp.parse('mortal(socrates)')
>>>c2 = lp.parse('-mortal(socrates)')
>>>mb=nltk.Mace(5)
>>>print mb.build_model(None,[a3, c1])
True
>>>print mb.build_model(None,[a3, c2])
True
>>>print mb.build_model(None,[c1, c2])
False

Mace4也會為我們尋找一個反例：

例如這個鏈表：

[There is a woman that every man loves, Adamis a man,Eveis a woman]

我們的結論是：

Adam loves Eve。

Mace4能找到使假設為真而結論為假的模型嗎？在下面的代碼，我們使用MaceCommand()檢查已建立的模型。

>>>a4 = lp.parse('exists y. (woman(y) &all x. (man(x) -> love(x,y)))')
>>>a5 = lp.parse('man(adam)')
>>>a6 = lp.parse('woman(eve)')
>>>g= lp.parse('love(adam,eve)')
>>>mc= nltk.MaceCommand(g, assumptions=[a4, a5, a6])
>>>mc.build_model()
True

Mace4發現了一個反例模型，其中Adam愛某個女人而不是Eve。

>>>print mc.valuation
{'C1':'b',
'adam': 'a',
'eve': 'a',
'love': set([('a', 'b')]),
'man': set([('a',)]),
'woman': set([('a',), ('b',)])}

此外，我們并沒有指定man和woman表示不相交的集合，因此，模型生成器讓它們相互重疊。

因此，讓我們添加一個新的假設，使man和woman不相交。模型生成器仍然產生一個反例模型，但這次更符合我們直覺的有關情況：

>>>a7 = lp.parse('all x.(man(x) -> -woman(x))')
>>>g= lp.parse('love(adam,eve)')
>>>mc= nltk.MaceCommand(g, assumptions=[a4, a5, a6, a7])
>>>mc.build_model()
True
>>>print mc.valuation
{'C1':'c',
'adam': 'a',
'eve': 'b',
'love': set([('a', 'c')]),
'man': set([('a',)]),
'woman': set([('b',), ('c',)])}

我們的假設中沒有說Eve是論域中唯一的女性，所以反例模型其實是可以接受的。如果想排除這種可能性，我們將不得不添加進一步的假設，如exists y. allx.(woman(x) ->(x =y))，以確保模型中只有一個女性。

總結

以上是生活随笔為你收集整理的【语言处理与Python】10.3一阶逻辑的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。