# IFF in ResolutionProover

33 views

### Amir Pourabdollah

Feb 20, 2021, 12:30:50 AMFeb 20
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])))
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])))
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])))
all x.(man(x) <-> mortal(x)), man(Socrates) |- mortall(Socrates): True
...which is strange!