• 3.8 模型的建立

    3.8 模型的建立

    我们一直假设我们已经有了一个模型，并要检查模型中的一个句子的真值。相比之下，模型的建立是给定一些句子的集合，尝试创造一种新的模型。如果成功，那么我们知道集合是一致的，因为我们有模型的存在作为证据。

    我们通过创建Mace()的一个实例并调用它的build_model()方法来调用 Mace4 模式产生器，与调用 Prover9 定理证明器类似的方法。一种选择是将我们的候选的句子集合作为假设，保留目标为未指定。下面的交互显示了[a, c1]和[a, c2]都是一致的列表，因为 Mace 成功的为它们都建立了一个模型，而[c1, c2]不一致。

    1. >>> a3 = read_expr('exists x.(man(x) & walks(x))')
    2. >>> c1 = read_expr('mortal(socrates)')
    3. >>> c2 = read_expr('-mortal(socrates)')
    4. >>> mb = nltk.Mace(5)
    5. >>> print(mb.build_model(None, [a3, c1]))
    6. True
    7. >>> print(mb.build_model(None, [a3, c2]))
    8. True
    9. >>> print(mb.build_model(None, [c1, c2]))
    10. False

    我们也可以使用模型建立器作为定理证明器的辅助。假设我们正试图证明S ⊢ g，即g是假设S = [s1, s2, ..., sn]的逻辑派生。我们可以同样的输入提供给 Mace4，模型建立器将尝试找出一个反例，就是要表明g 不 遵循从S。因此，给定此输入，Mace4 将尝试为假设S连同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。Mace4 能找到使假设为真而结论为假的模型吗？在下面的代码中，我们使用MaceCommand()检查已建立的模型。

    1. >>> a4 = read_expr('exists y. (woman(y) & all x. (man(x) -> love(x,y)))')
    2. >>> a5 = read_expr('man(adam)')
    3. >>> a6 = read_expr('woman(eve)')
    4. >>> g = read_expr('love(adam,eve)')
    5. >>> mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6])
    6. >>> mc.build_model()
    7. True

    因此答案是肯定的：Mace4 发现了一个反例模型，其中 Adam 爱某个女人而不是 Eve。但是，让我们细看 Mace4 的模型，转换成我们用来估值的格式。

    1. >>> print(mc.valuation)
    2. {'C1': 'b',
    3.  'adam': 'a',
    4.  'eve': 'a',
    5.  'love': {('a', 'b')},
    6.  'man': {('a',)},
    7.  'woman': {('a',), ('b',)}}

    这个估值的一般形式应是你熟悉的：它包含了一些单独的常量和谓词，每一个都有适当类型的值。可能令人费解的是C1。它是一个“Skolem 常量”，模型生成器作为存在量词的表示引入的。也就是说，模型生成器遇到a4里面的exists y，它知道，域中有某个个体b满足a4中的开放公式。然而，它不知道b是否也是它的输入中的某个地方的一个独立常量的标志，所以它为b凭空创造了一个新名字，即C1。现在，由于我们的假设中没有关于独立常量adam和eve的信息，模型生成器认为没有任何理由将它们当做表示不同的实体，于是它们都得到映射到a。此外，我们并没有指定man和woman表示不相交的集合，因此，模型生成器让它们相互重叠。这个演示非常明显的隐含了我们用来解释我们的情境的知识，而模型生成器对此一无所知。因此，让我们添加一个新的假设，使 man 和 woman 不相交。模型生成器仍然产生一个反例模型，但这次更符合我们直觉的有关情况：

    1. >>> a7 = read_expr('all x. (man(x) -> -woman(x))')
    2. >>> g = read_expr('love(adam,eve)')
    3. >>> mc = nltk.MaceCommand(g, assumptions=[a4, a5, a6, a7])
    4. >>> mc.build_model()
    5. True
    6. >>> print(mc.valuation)
    7. {'C1': 'c',
    8.  'adam': 'a',
    9.  'eve': 'b',
    10.  'love': {('a', 'c')},
    11.  'man': {('a',)},
    12.  'woman': {('c',), ('b',)}}

    经再三考虑，我们可以看到我们的假设中没有说 Eve 是论域中唯一的女性，所以反例模型其实是可以接受的。如果想排除这种可能性，我们将不得不添加进一步的假设，如exists y. all x. (woman(x) -> (x = y))以确保模型中只有一个女性。