使用NLTK简化逻辑表达式

Question

我对使用自然语言工具包（NLTK）有疑问。我正在尝试创建一个应用程序，以便将自然语言问题转换为其逻辑表示形式，并查询数据库。

我使用nltk.sem.logic包下的简化（）方法后得到了，得到了下面的表达式结果：

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

但我需要的是把它简化为：

owner(fido, z0) 

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

Answer 1

在NLTK中，simplify()执行beta缩减（according to the book），这不是您所需要的。当你应用某些策略时，你所问的只能用定理证明。在这种情况下，你需要知道你期望得到的结果，或者你知道可以应用什么样的公理来获得这样的结果。

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蟒蛇：

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 

UPDATE

如果你坚持使用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)>