36 views

Skip to first unread message

Feb 20, 2021, 12:30:50 AM2/20/21

to nltk-users

Hello

In the ResolutionProver it seems to me that having IFF implication makes wrong inference. Please let me kow if I missed anything. Here is the example adapted from the demo part at https://www.nltk.org/_modules/nltk/inference/resolution.html :

Original example:

p1 = Expression.fromstring(r"all x.(man(x) **->** mortal(x))")

p2 = Expression.fromstring(r"man(Socrates)")

c = Expression.fromstring(r"mortal(Socrates)")

print("%s, %s |- %s: %s" % (p1, p2, c, ResolutionProver().prove(c, [p1, p2])))

p2 = Expression.fromstring(r"man(Socrates)")

c = Expression.fromstring(r"mortal(Socrates)")

print("%s, %s |- %s: %s" % (p1, p2, c, ResolutionProver().prove(c, [p1, p2])))

Output:

all x.(man(x) <-> mortal(x)), man(Socrates) |- -mortal(Socrates): True

I changed it to:

p1 = Expression.fromstring(r"all x.(man(x) **<->** mortal(x))")

p2 = Expression.fromstring(r"man(Socrates)")

c = Expression.fromstring(r"**-**mortal(Socrates)")

print("%s, %s |- %s: %s" % (p1, p2, c, ResolutionProver().prove(c, [p1, p2])))

p2 = Expression.fromstring(r"man(Socrates)")

c = Expression.fromstring(r"

print("%s, %s |- %s: %s" % (p1, p2, c, ResolutionProver().prove(c, [p1, p2])))

Output:

all x.(man(x) <-> mortal(x)), man(Socrates) |- -mortal(Socrates): **True**

Basically I changed the IF to IFF and asked for checking a false statement. I expected the above to be logically **Flase**. In fact any c leads to true even for c=None. I digged into the issue and realised that when the IFF is split into two IFs in the code, the two clauses are taken as contradictory in the inference loop. It means that any KB with IFF is taken as having an internal contradiction, therefore any inference leads to True regardless of c. For example:

p1 = Expression.fromstring(r"all x.(man(x) <-> mortal(x))")

p2 = Expression.fromstring(r"man(Socrates)")

c = None

print("%s, %s |- %s: %s" % (p1, p2, c, ResolutionProver().prove(c, [p1, p2])))

leads to:

p2 = Expression.fromstring(r"man(Socrates)")

c = None

print("%s, %s |- %s: %s" % (p1, p2, c, ResolutionProver().prove(c, [p1, p2])))

leads to:

all x.(man(x) <-> mortal(x)), man(Socrates) |- mortall(Socrates): **True**

...which is strange!

Please help me if this is a bug or I missed anything!

Thanks

Amir.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu