NLTKを使用した論理式の簡略化

Question

Natural Language ToolKit（NLTK）の使用に疑問があります。自然言語の質問をロジック表現に変換し、データベースにクエリするためにアプリケーションを作成しようとしています。

私はnltk.sem.logicパッケージの下の簡素化（）メソッドを使用した後に得て、次の式だ結果：

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

をしかし、私は必要なのフォローとして、それを簡単にすることである。

owner(fido, z0) 

文章を減らす方法がありますか？

Answer 1

NLTKでは、simplify()は、必要なものではないベータ還元（according to the book）を実行します。あなたが何を求めているのかは、あなたが特定の戦術を適用するときに定理証明者だけが行うことができます。この場合、最終的に得られると予想されることを知る必要がありますか、そのような結果を得るためにどのような公理を適用できるかを知っています。

NLTKの定理証明はProver9であり、同値関係をチェックするツールを提供します。基本的には、式（敷地）のリストから目標式までのステップ数が限られた校正があるかどうかだけを確認することができます。 NLTKのpythonで

============================== 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 ========================== 

：

あなたが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 

UPDATE

例えばあなたのケースでは、これは結果でしたこの特定のパターンを正規表現で手動でチェックします。おそらく、正規表現を使用してこのような何かを行うことができます（私が承認したがのが私の厄介な戦術を試してみましょうしないでください）：

は

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