I have a doubt at using Natural Language ToolKit (NLTK). I'm trying to make an app in order to translate a Natural Language Question into it's logic representation, and query to a database.
The result I got after using the simplify() method under nltk.sem.logic package and got the following expression:
exists z2.(owner(fido, z2) & (z0 = z2))
simplify() performs beta reduction (according to the book) which is not what you need. What you are asking is only doable with theorem provers when you apply certain tactics. Which in this case, you either need to know what you expect to get at the end or you know what kinds of axioms can be applied to get such result.
The theorem prover in NLTK is Prover9 which provides tools to check entailment relations. Basically, you can only check if there is a proof with a limited number of steps from a list of expressions (premises) to a goal expression. In your case for example, this was the result:
============================== 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 ==========================
In 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
In case that you insist on using available tools in python and you want to manually check this certain pattern with regular expressions. You can probably do something like this with regular expression (I don't approve but let's try my nasty tactic):
def my_nasty_tactic(exp): parameter = re.findall(r'exists ([^.]*)\..*', exp) if len(parameter) == 1: parameter = parameter substitution = re.findall(r'&[ ]*\([ ]*([^ ]+)[ ]*=[ ]*'+parameter+r'[ ]*\)', exp) if len(substitution) == 1: substitution = substitution 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()
Then you can use it like this:
my_nasty_tactic('exists z2.(owner(fido, z2) & (z0 = z2))') # <ApplicationExpression owner(fido,z0)>