使用NLTK简化逻辑表达式

Question

我对使用自然语言ToolKit (NLTK)有疑问。我正在尝试开发一个应用程序，以便将一个自然语言问题转化为它的逻辑表示，并对数据库进行查询。

在nltk.sem.logic包中使用simplify()方法后得到的结果得到了以下表达式：

exists z2.(owner(fido, z2) & (z0 = z2))

但我需要的是简化如下：

owner(fido, z0)

还有另一种方法可以减少我想要的句子吗？

Answer 1

在NLTK中，simplify()执行贝塔缩减(根据这本书)，这不是您所需要的。当你运用某些策略时，你所要求的只有用定理证明器才能做到。在这种情况下，您要么需要知道您希望在最后得到什么，要么您知道可以应用什么样的公理来获得这样的结果。

NLTK中的定理证明器是Prover9，它提供了检验包含关系的工具。基本上，您只能检查是否有从表达式列表(前提)到目标表达式的步骤数量有限的证据。例如，在您的案例中，结果是：

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.00 (+ 0.00) seconds.
% Length of proof is 8.
% Level of proof is 4.
% Maximum clause weight is 4.
% Given clauses 0.

1 (exists x (owner(fido,x) & y = x)) # label(non_clause).  [assumption].
2 owner(fido,x) # label(non_clause) # label(goal).  [goal].
3 owner(fido,f1(x)).  [clausify(1)].
4 x = f1(x).  [clausify(1)].
5 f1(x) = x.  [copy(4),flip(a)].
6 -owner(fido,c1).  [deny(2)].
7 owner(fido,x).  [back_rewrite(3),rewrite([5(2)])].
8 $F.  [resolve(7,a,6,a)].

============================== end of proof ==========================

在NLTK python中：

from nltk import Prover9
from nltk.sem import Expression
read_expr = Expression.fromstring
p1 = read_expr('exists z2.(owner(fido, z2) & (z0 = z2))')
c = read_expr('owner(fido, z0)')
result = Prover9().prove(c, [p1])
print(result)
# returns True

更新

如果您坚持在python中使用可用的工具，并且希望用正则表达式手动检查这个特定的模式。您可能可以使用正则表达式来做这样的事情(我不赞成，但让我们试试我的讨厌的策略)：

def my_nasty_tactic(exp):
    parameter = re.findall(r'exists ([^.]*)\..*', exp)
    if len(parameter) == 1:
        parameter = parameter[0]
        substitution = re.findall(r'&[ ]*\([ ]*([^ ]+)[ ]*=[ ]*'+parameter+r'[ ]*\)', exp)
        if len(substitution) == 1:
             substitution = substitution[0]
             exp_abs = re.sub(r'exists(?= [^.]*\..*)', "\ ", exp)
             exp_abs = re.sub(r'&[ ]*\([ ]*' + substitution + '[ ]*=[ ]*'+parameter+r'[ ]*\)', '', exp_abs)
             return read_expr('(%s)(%s)' % (exp_abs, substitution)).simplify()

然后你可以像这样使用它：

my_nasty_tactic('exists z2.(owner(fido, z2) & (z0 = z2))')
# <ApplicationExpression owner(fido,z0)>