• 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

    我们也可以使用模型建立器作为定理证明器的辅助。假设我们正试图证明Sg,即g是假设S = [s1, s2, ..., sn]的逻辑派生。我们可以同样的输入提供给 Mace4,模型建立器将尝试找出一个反例,就是要表明g 遵循从S。因此,给定此输入,Mace4 将尝试为假设S连同g的否定找到一个模型,即列表S' = [s1, s2, ..., sn, -g]。如果gS不能证明出来,那么 Mace4 会返回一个反例,比 Prover9 更快的得出结论:无法找到所需的证明。相反,如果gS是可以证明出来,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。现在,由于我们的假设中没有关于独立常量adameve的信息,模型生成器认为没有任何理由将它们当做表示不同的实体,于是它们都得到映射到a。此外,我们并没有指定manwoman表示不相交的集合,因此,模型生成器让它们相互重叠。这个演示非常明显的隐含了我们用来解释我们的情境的知识,而模型生成器对此一无所知。因此,让我们添加一个新的假设,使 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))以确保模型中只有一个女性。