IFF in ResolutionProover

[Amir Pourabdollah]

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