3.1 句法

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

>>> read_expr = nltk.sem.Expression.fromstring
>>> expr = read_expr('walk(angus)', type_check=True)
>>> expr.argument
<ConstantExpression angus>
>>> expr.argument.type
e
>>> expr.function
<ConstantExpression walk>
>>> expr.function.type
<e,?>

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

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

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

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

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

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