Hello
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.