<jupyter_start><jupyter_text>一阶逻辑本节我们将通过翻译自然语言表达式为一阶逻辑来表示它们的意思。并不是所有的自然语言语义都可以用一阶逻辑表示，但它是计算语义的一个不错的选择，因为它具有足够的表现力来表达语义的很多方面，而且另一方面，有出色的现成系统可用于开展一阶逻辑的自动推理。 句法一阶逻辑保留所有命题逻辑的**布尔运算符**，但它增加了一些重要的新机制。一阶逻辑的标准构造规则包括以下术语：独立变量、独立常量、带不同数量的参数的**谓词**。例如：Angus walks 可以被形式化为 walk(angus)，Angus sees Bertie 可以被形式化为 see(angus, bertie)。我们称 walk 为**一元谓词**，see 为**二元谓词**。一阶逻辑本身没有什么实质性的关于词汇语义的表示，原子谓词如 see(angus, berties) 在某种情况下是真还是假并不是一个逻辑问题，而依赖于特定的估值，即我们为常量 see、angus 和 bertie 选择的值，因此这些表达式被称为**非逻辑常量**。与之相反，**逻辑常量**（如布尔运算符）在一阶逻辑的每个模型中的解释总是相同的。我们应该在这里提到：有一个二元谓词具有特殊的地位，它就是等号，如在 angus = aj 这样的公式中的等号。等号被视为一个逻辑常量，因为对于任何 t1 和 t2，公式 t1 = t2 为真当且仅当 t1 和 t2 指向同一个实体。按照 Montague 文法的约定，我们将使用两种基本类型来表示一阶逻辑：**e**为实体类型，而**t**为公式类型，即具有真值的表达式。给定这两种基本类型，我们可以构造函数表达式的**复杂类型**，也就是说给定任何类型 σ 和 τ， 是一个对应与从 σ 类型到 τ 类型的函数的复杂类型。例如  是从实体到真值的表达式类型，也就是一元谓词，可以通过下面的方式来进行类型检查：<jupyter_code>import nltk
read_expr = nltk.sem.Expression.fromstring
expr = read_expr('walk(angus)', type_check=True)
print(expr.argument)
print(expr.argument.type)
print(expr.function)
print(expr.function.type)<jupyter_output>angus
e
walk
<e,?><jupyter_text>为什么我们在最后看到了  呢？虽然类型检查器会尝试推断出尽可能多的类型，但在这种情况下，它并没有能够推断出 walk 的类型，所以其结果类型是未知的。为了帮助类型检查器，我们可以指定一个**信号**，即实现一个字典，明确指出非逻辑常量的类型：<jupyter_code>sig = {'walk': '<e, t>'}
expr = read_expr('walk(angus)', signature=sig)
print(expr.function.type)<jupyter_output>e<jupyter_text>在一阶逻辑中，谓词的参数也可以是独立变量，如 x、y 和 z。独立变量类似人称代词，如 he、she 和 it，我们需要联系上下文来弄清楚它们的含义。为了解释 He disappeared. 这个句子中 he 指代的是什么，我们有两种做法：一种方法是直接将其指向一个相关的本地对象；另一种方法是为代词提供文本中的先行词，例如将句子 Cyril is Angus's dog. 放在 He disappeared. 前面，那么 He disappeared. 在语义上就和 Cyril disappeared. 等价。    再思考下面例子中的 he，在这种情况下，它收不确定的 NP（a dog）的约束，这是一个和共指关系不同的关系。如果我们替换代词 he 为 a dog，结果 b 就在语义上与 a 不等效。    a. Angus had a dog but he disappeared.    b. Angus had a dog but a dog disappeared.    对应下面的句子 a，我们可以构建一个**开放公式** b，其中变量 x 出现了两次：        a. He is a dog and he disappeared.    b. dog(x) & disappear(x)    通过在上面的开放公式前面指定一个**存在量词 ∃x**（存在某些 x），我们可以**绑定**这些变量，下面的例子中 a 的意思是 b，更习惯的写法是 c：    a. ∃x.(dog(x) & disappear(x))    b. At least one entity is a dog and disappeared.    c. A dog disappeared.    NLTK 中的写法是 exists x.(dog(x) & disappear(x))。除了存在量词，一阶逻辑还为我们提供了**全称量词 ∀x**（对所有 x）：    a. ∀x.(dog(x) -> disappaer(x))    b. Everything has the property that if it is a dog, it disappears.    c. Every dog disappeared.    NLTK 中的写法是 all x.(dog(x) -> disappear(x))。考虑下面两组公式：    a. ((exists x. dog(x)) -> bark(x)    b. all x. ((exists x. dog(x)) -> bark(x))    在公式 a 中，存在量词 x 的范围是 dog(x)，所以 bark(x) 中的 x 的出现是不受限制的。因此，它可以被其他一些量词约束，如公式 b 所示。在一般情况下，变量 x 在公式 φ 中是**自由**的，如果它没有出现在 all x 或 exists x 的范围内。相反，如果 x 出现在了 all x 或 exists x 范围内，它就是**受限**的。如果公式中所有的变量都是受限的，那么我们说这个公式是**封闭**的。我们可以通过 Expression 对象的 free() 方法返回公式中自由变量的集合：<jupyter_code>print(read_expr('dog(cyril)').free())
print(read_expr('dog(x)').free())
print(read_expr('own(angus, cyril)').free())
print(read_expr('exists x. dog(x)').free())
print(read_expr('((some x. walk(x)) -> sing(x))').free())
print(read_expr('exists x. own(y, x)').free())<jupyter_output>set()
{Variable('x')}
set()
set()
{Variable('x')}
{Variable('y')}<jupyter_text>一阶定理证明回顾前面我们在 to the north of 上遇到的限制：    if x is to the north of y then y is not to the north of x.    命题逻辑不足以表示与二元谓词相关的概括，因此，我们不能正确地捕获以下论证：    Sylvania is to the north of Freedonia. Therefore, Freedonia is not to the north of Sylvania.    毫无疑问，用一阶逻辑形式化这些规则是很理想的：    all x. all y. (north_of(x, y) -> -north_of(y, x))    更妙的是，我们可以进行自动推理来证明论证的有效性。定理证明在一般情况下是为了确定我们要证明的公式（**证明目标**）是否可以从一系列假设的公式经过有限的推理步骤派生出来，写作 S ⊢ g，其中 S 是假设列表（可以为空），g 是证明目标。下面我们用 NLTK 中的定理证明接口 Prover9 来演示：<jupyter_code>NotFnS = read_expr('-north_of(f, s)')
SnF = read_expr('north_of(s, f)')
R = read_expr('all x. all y. (north_of(x, y) -> -north_of(y, x))')
prover = nltk.Prover9()
prover.prove(NotFnS, [SnF, R])<jupyter_output><empty_output><jupyter_text>定理证明器证明我们的论证是有效的，反过来，也可以用来验证不能从我们的假设推导出 north_of(f, s)：<jupyter_code>FnS = read_expr('north_of(f, s)')
prover.prove(FnS, [SnF, R])<jupyter_output><empty_output><jupyter_text>一阶逻辑语言总结下面我们来总结一阶逻辑的句法。我们采取约定： 是一种由 n 个类型为 e 的参数组成的产生一个类型为 t 的表达式的谓词类型，n 是谓词的**元数**：1. 如果 P 是类型  的谓词，a1,...,an 是 e 类型的术语，那么 P(a1,...,an) 的类型是 t。2. 如果 α 和 β 都是 e 类型的，那么 (α = β) 和 (α != β) 都是 t 类型的。3. 如果 φ 是 t 类型的，那么 -φ 也是 t 类型的。4. 如果 φ 和 ψ 是 t 类型的，那么 (φ & ψ)，(φ | ψ)，(φ -> ψ) 和 (φ  ψ) 也是 t 类型的。5. 如果 φ 是 t 类型的，x 是类型为 e 的变量，那么 exists x. φ 和 all x. φ 也是 t 类型的。下表总结了一阶逻辑的几个新逻辑关系和 Expression 类的两个实用方法：| 示例         | 描述         ||--------------|--------------|| =            | 等于         || !=           | 不等于       || exists       | 存在量词     || all          | 全称量词     || e.free()     | e 的自由变量 || e.simplify() | e 的简化形式 |  真值模型现在，我们来给出一阶逻辑的真值条件的语义：给定一阶逻辑语言 L，L 的模型 M 是一个  对，其中 D 是一个非空集合，称为模型的**域**，Val 是一个函数，称为**估值函数**，它按如下方式从 D 中分配值给 L 的表达式：1. 对于 L 中的每一个独立常量 c，Val(c) 是 D 中的元素。2. 对于每一个元数 n >= 0 的谓词符号 P，Val(P) 是从 D^n 到 {True, False} 的函数（如果 P 的元数为 0，则 Val(P) 是一个简单的真值，P 被认为是一个命题符号）。在 NLTK 中我们采用更简单的定义，定义 Val(P) 为集合 S:        S = {s | f(s) = True}    这样的 f 被称为 S 的**特征函数**。现在假设我们有一个域 dom 包括 Bertie、Olive 和 Cyril，其中 Bertie 是男孩，Olive 是女孩，而 Cyril 是小狗。为了方便记录，我们用 b、o 和 c 作为模型中对应的标签，并定义如下估值：<jupyter_code>dom = {'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.Valuation.fromstring(v)
print(val)<jupyter_output>{'bertie': 'b',
 'boy': {('b',)},
 'cyril': 'c',
 'dog': {('c',)},
 'girl': {('o',)},
 'olive': 'o',
 'see': {('o', 'c'), ('c', 'b'), ('b', 'o')},
 'walk': {('o',), ('c',)}}<jupyter_text>根据这一估值，see 的值是一个元组集合，包含：Bertie 看到 Olive、Cyril 看到 Bertie、Olive 看到 Cyril。同时，一元谓词（如 boy、girl、dog）也是以单个元组的集合而不是个体的集合出现的，这使我们能够方便地统一处理任何元数的关系。一个形式为 P(T1,...Tn) 的谓词，其中 P 是 n 元的，其为真的条件是对应于 (T1,...Tn) 的值的元组属于 P 的元组集合：<jupyter_code>print(('o', 'c') in val['see'])
print(('b',) in val['boy'])<jupyter_output>True
True<jupyter_text>独立变量和赋值在我们的模型中，上下文的使用对应的是为变量**赋值**，这是一个从独立变量到域中实体的映射。[nltk.Assignment](https://www.nltk.org/_modules/nltk/sem/evaluate.htmlAssignment) 提供了赋值的功能，它以模型的域为参数，并按照（变量，值）的形式进行绑定：<jupyter_code>g = nltk.Assignment(dom, [('x', 'o'), ('y', 'c')])
g<jupyter_output><empty_output><jupyter_text>接下来我们创建一个模型，然后调用 evaluate() 方法计算真值：<jupyter_code>m = nltk.Model(dom, val)
m.evaluate('see(olive, y)', g)<jupyter_output><empty_output><jupyter_text>由于我们已经知道 o 和 c 在 see 关系中表示的含义，所以 True 值是我们所期望的，在这种情况下，我们可以说赋值 g 满足公式 see(olive, y)。相比之下，下面的公式相对于 g 的评估结果为 False：<jupyter_code>m.evaluate('see(y, x)', g)<jupyter_output><empty_output><jupyter_text>我们可以使用方法 purge() 清除一个赋值中所有的绑定：<jupyter_code>g.purge()
g<jupyter_output><empty_output><jupyter_text>如果现在我们再尝试为公式 see(olive, y) 相对于 g 估值计算真值，就会得到 Undefined：<jupyter_code>m.evaluate('see(olive, y)', g)<jupyter_output><empty_output><jupyter_text>由于我们的模型已经包含了解释布尔运算的规则，因此任何复杂的公式都可以进行组合和评估：<jupyter_code>m.evaluate('see(bertie, olive) & boy(bertie) & -walk(bertie)', g)<jupyter_output><empty_output><jupyter_text>量化现代逻辑的关键特征之一就是变量满足的概念可以用来解释量化的公式，例如：exists x. (girl(x) & walk(x)) 什么时候为真？我们要检查域中的个体中是否有属性是女孩并且走路的，也就是说 dom 中是否存在某个 u 使 g[u/x] 满足开放公式 girl(x) & walk(x)：<jupyter_code>m.evaluate('exists x. (girl(x) & walk(x))', g)<jupyter_output><empty_output><jupyter_text>这里 evaluate() 返回了 True, 因为 dom 中的 o 满足开放公式。NLTK 中提供了一个有用的工具：satisfiers() 方法，它返回满足开放公式的所有个体集合，其参数是一个已分析的公式、一个变量和一个赋值。<jupyter_code>fmla1 = read_expr('girl(x) | boy(x)')
print(m.satisfiers(fmla1, 'x', g))
fmla2 = read_expr('girl(x) -> walk(x)')
print(m.satisfiers(fmla2, 'x', g))
fmla3 = read_expr('walk(x) -> girl(x)')
print(m.satisfiers(fmla3, 'x', g))<jupyter_output>{'o', 'b'}
{'o', 'c', 'b'}
{'o', 'b'}<jupyter_text>以 fmla2 为例，girl(x) -> walk(x) 等价于 -girl(x) | walk(x)，即要么不是女孩，要么在步行的个体都满足条件，因此 Bertie、Cyril 和 Olive 都满足条件。同时，由于域 dom 中的每一个成员都满足 fmla2，那么相应的全称量化公式也为真：<jupyter_code>m.evaluate('all x. (girl(x) -> walk(x))', g)<jupyter_output><empty_output><jupyter_text>量词范围歧义对于句子 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)))    这两个的含义不同，公式 b 声称只有一个人被所有人钦佩，而公式 a 只要其对于每一个 x 我们可以找到 x 钦佩的一些人 y 即可，每次找到的人 y 可以不同。我们使用术语**量化范围**来区分它们，在公式 a 中 ∀ 比 ∃ 具有更广的量化范围，而公式 b 则相反。这两种一阶逻辑表达式都是合理的，因此我们称原句子关于量化范围有歧义。为了更仔细地检查歧义，我们定义如下估值：<jupyter_code>v2 = """
    bruce => b
    elspeth => e
    julia => j
    matthew => m
    person => {b, e, j, m}
    admire => {(j, b), (b, b), (m, e), (e, m)}
"""
val2 = nltk.Valuation.fromstring(v2)<jupyter_output><empty_output><jupyter_text>其中的 admire 关系可以用下面的映射图进行可视化，其中 b 和 j 都钦佩 b，而 e 和 m 互相钦佩。![models_admire.png](resources/models_admire.png)在这样的估值下，前面提到的公式 b 为真而公式 a 为假。我们使用 Model 对象的 satisfiers() 方法进行进一步的探索：<jupyter_code>dom2 = val2.domain
m2 = nltk.Model(dom2, val2)
g2 = nltk.Assignment(dom2)
fmla4 = read_expr('(person(x) -> exists y. (person(y) & admire(x, y)))')
m2.satisfiers(fmla4, 'x', g2)<jupyter_output><empty_output><jupyter_text>这表明 fmla4 包含域中的每一个个体，相反，下面的公式 fmla5 则没有满足的 y 值。<jupyter_code>fmla5 = read_expr('(person(y) & all x. (person(x) -> admire(x, y)))')
m2.satisfiers(fmla5, 'y', g2)<jupyter_output><empty_output><jupyter_text>也就是说，没有大家都钦佩的人。看看另一个开放公式 fmla6，可以验证有一个人，即 Bruce，他被 Julia 和 Bruce 都钦佩。<jupyter_code>fmla6 = read_expr('(person(y) & all x. ((x = bruce | x = julia) -> admire(x, y)))')
m2.satisfiers(fmla6, 'y', g2)<jupyter_output><empty_output><jupyter_text>模型的建立前面一致假设我们已经有了一个模型，并要检查模型中的一个句子的真值。相比之下，模型的建立是给定一些句子的集合，尝试创造一种新的模型。如果成功，那么我们知道集合是一致的，因为我们有模型的存在作为证据。我们通过创建 [nltk.Mace](http://www.nltk.org/_modules/nltk/inference/mace.htmlMace) 的一个实例并调用它的 build_model() 方法来调用 Mace4 产生器。下面的例子显示了公式 a3 和 c1 一致，a3 和 c2 也一致，但是 c1 和 c2 不一致：<jupyter_code>a3 = read_expr('exists x. (man(x) & walks(x))')
c1 = read_expr('mortal(socrates)')
c2 = read_expr('-mortal(socrates)')
mb = nltk.Mace(5)
print(mb.build_model(None, [a3, c1]))
print(mb.build_model(None, [a3, c2]))
print(mb.build_model(None, [c1, c2]))<jupyter_output>True
True
False<jupyter_text>我们也可以使用模型建立器作为定理证明器的辅助。假设我们试图证明 S ⊢ g，即 g 是假设 S = [s1, s2, ..., sn]  的逻辑派生。我们把同样的输入提供给 Mace4，Mace4 将尝试为假设 A 连同 g 的否定找到一个模型，即 S' =[s1, s2, ..., sn, -g]。如果 g 不能从 S 证明出来，那么 Mace4 就会返回一个反例，可以比 Prover9 更快地得出结论；相反，如果 g 可以从 S 证明出来，Mace4 可能要花很长时间不能成功地找到一个反例模型，最终放弃。让我们思考一个具体的方案，我们的假设是 There is a woman that every man loves，Adam is a man 和 Eve is a woman，结论是 Adam loves Eve。在下面的代买中，我们使用 [nltk.MaceCommand](http://www.nltk.org/_modules/nltk/inference/mace.htmlMaceCommand) 检查已建立的模型：<jupyter_code>a4 = read_expr('exists y. (woman(y) & all x. (man(x) -> love(x, y)))')
a5 = read_expr('man(adam)')
a6 = read_expr('woman(eve)')
g = read_expr('love(adam, eve)')
mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6])
mc.build_model()<jupyter_output><empty_output><jupyter_text>让我们细看 Mace4 的模型，转换成估值的形式：<jupyter_code>print(mc.valuation)<jupyter_output>{'C1': 'b',
 'adam': 'a',
 'eve': 'a',
 'love': {('a', 'b')},
 'man': {('a',)},
 'woman': {('a',), ('b',)}}<jupyter_text>这个估值形式包含了一些单独的常量和谓词，每一个都有适当类型的值。其中 C1 是模型生成器作为存在量词的表示引入的，当模型生成器遇到 a4 里面的 exists y，它知道域中有某个个体 b 满足 a4 中的开放公式，然而它不知道 b 是否也是它的输入中某个地方的一个独立常量的标志，所以它为 b 凭空创造了一个新名字 C1。现在，由于我们的假设中没有关于独立常量 adam 和 eve 的信息，模型生成器认为没有任何理由将它们当作表示不同的实体，于是它们都被映射到 a。此外，我们并没有指定 man 和 woman 表示不相交的集合，因此模型生成器让它们相互重叠。现在我们添加一个新的假设，使 man 和 woman 不相交：<jupyter_code>a7 = read_expr('all x. (man(x) -> -woman(x))')
g = read_expr('love(adam, eve)')
mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6, a7])
mc.build_model()<jupyter_output><empty_output><jupyter_text>此时，man 和 woman 就被映射到了不同的变量。<jupyter_code>print(mc.valuation)<jupyter_output>{'C1': 'c',
 'adam': 'a',
 'eve': 'b',
 'love': {('a', 'c')},
 'man': {('a',)},
 'woman': {('c',), ('b',)}}
{'fraction_non_alphanumeric': 0.1757802312440233, 'fraction_numerical': 0.008519516647831, 'mean_word_length': 6.123219814241486, 'pattern_counts': {'":': 0, '<': 94, '<?xml version=': 0, '>': 128, 'https://': 1, 'lorem ipsum': 0, 'www.': 3, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '25', 'dir': 'jupyter-structured-clean-dedup', 'id': '499045', 'license': 'MIT', 'n_tokens_mistral': 7285, 'n_tokens_neox': 7697, 'n_words': 1010, 'path': '10.3-first-order-logic.ipynb', 'repo_name': 'pen-x/natural-language-processing-with-python', 'size': '11503'}