• 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))