这一节，通过翻译自然语言表达式为一阶逻辑来表示它们的意思。

并不是所有的自然语言语义都可以用一阶逻辑来表示。

句法

一阶逻辑保留了所有命题逻辑的布尔运算符但是它增加了一些重要的新机制。

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))，以确保模型中只有一个女性。