• 3.1 句法

    3.1 句法

    一阶逻辑保留所有命题逻辑的布尔运算符。但它增加了一些重要的新机制。首先,命题被分析成谓词和参数,这将我们与自然语言的结构的距离拉近了一步。一阶逻辑的标准构造规则承认以下术语:独立变量和独立常量、带不同数量的参数的谓词。例如,Angus walks 可以被形式化为 walk(angus),Angus sees Bertie 可以被形式化为 see(angus, bertie)。我们称 walk 为一元谓词,see 为二元谓词。作为谓词使用的符号不具有内在的含义,虽然很难记住这一点。回到我们前面的一个例子,(13a)和(13b)之间没有逻辑区别。

    1. >>> read_expr = nltk.sem.Expression.fromstring
    2. >>> expr = read_expr('walk(angus)', type_check=True)
    3. >>> expr.argument
    4. <ConstantExpression angus>
    5. >>> expr.argument.type
    6. e
    7. >>> expr.function
    8. <ConstantExpression walk>
    9. >>> expr.function.type
    10. <e,?>

    为什么我们在这个例子的结尾看到&lt;e,?&gt;呢?虽然类型检查器会尝试推断出尽可能多的类型,在这种情况下,它并没有能够推断出walk的类型,所以其结果的类型是未知的。虽然我们期望walk的类型是&lt;e, t&gt;,迄今为止类型检查器知道的,在这个上下文中可能是一些其他类型,如&lt;e, e&gt;&lt;e, &lt;e, t&gt;。要帮助类型检查器,我们需要指定一个信号,作为一个字典来实施,明确的与非逻辑常量类型关联:

    1. >>> sig = {'walk': '<e, t>'}
    2. >>> expr = read_expr('walk(angus)', signature=sig)
    3. >>> expr.function.type
    4. e

    一种二元谓词具有类型〈e, 〈e, t〉〉。虽然这是先组合类型 e 的一个参数成一个一元谓词的类型,我们可以用二元谓词的两个参数直接组合来表示二元谓词。例如,在<cite>Angus sees Cyril</cite>的翻译中谓词 see 会与它的参数结合得到结果 see(angus, cyril)。

    在一阶逻辑中,谓词的参数也可以是独立变量,如 x,y 和 z。在 NLTK 中,我们采用的惯例:e 类型的变量都是小写。独立变量类似于人称代词,如 he,she 和 it ,其中我们为了弄清楚它们的含义需要知道它们使用的上下文。

    解释(14)中的代名词的方法之一是指向上下文中相关的个体。

    1. ((exists x. dog(x)) -> bark(x))