Super basic question. I am trying to express a symmetric relationship between two binary predicates (parent and child). But, with the following statement, my resolution prover allows me to prove anything. The converted CNF form makes sense to me as does the proof by resolution, but this should be an obvious case for false. What am I missing?
forall x,y (is-parent-of(x,y) <-> is-child-of(y,x))
I am using the nltk python library and the ResolutionProver prover. Here is the nltk code:
from nltk.sem import Expression as exp
from nltk.inference import ResolutionProver as prover
s = exp.fromstring('all x.(all y.(parentof(y, x) <-> childof(x, y)))')
q = exp.fromstring('foo(Bar)')
print prover().prove(q, [s], verbose=True)
output:
[1] {-foo(Bar)} A
[2] {-parentof(z9,z10), childof(z10,z9)} A
[3] {parentof(z11,z12), -childof(z12,z11)} A
[4] {} (2, 3)
True
Here is a quick fix for the ResolutionProver.
The issue that causes the prover to be unsound is that it does not implement the resolution rule correctly when there is more than one complementary literal. E.g. given the clauses {A B C} and {-A -B D} binary resolution would produce the clauses {A -A C D} and {B -B C D}. Both would be discarded as tautologies. The current NLTK implementation instead would produce {C D}.
This was probably introduced because clauses are represented in NLTK as lists, therefore identical literals may occur more than once within a clause. This rule does correctly produce an empty clause when applied to the clauses {A A} and {-A -A}, but in general this rule is not correct.
It seems that if we keep clauses free from repetitions of identical literals we can regain soundness with a few changes.
First define a function that removes identical literals.
Here is a naive implementation of such a function
import nltk.inference.resolution as res
def _simplify(clause):
"""
Remove duplicate literals from a clause
"""
duplicates=[]
for i,c in enumerate(clause):
if i in duplicates:
continue
for j,d in enumerate(clause[i+1:],start=i+1):
if j in duplicates:
continue
if c == d:
duplicates.append(j)
result=[]
for i,c in enumerate(clause):
if not i in duplicates:
result.append(clause[i])
return res.Clause(result)
Now we can plug this function into some of the functions of the nltk.inference.resolution module.
def _iterate_first_fix(first, second, bindings, used, skipped, finalize_method, debug):
"""
This method facilitates movement through the terms of 'self'
"""
debug.line('unify(%s,%s) %s'%(first, second, bindings))
if not len(first) or not len(second): #if no more recursions can be performed
return finalize_method(first, second, bindings, used, skipped, debug)
else:
#explore this 'self' atom
result = res._iterate_second(first, second, bindings, used, skipped, finalize_method, debug+1)
#skip this possible 'self' atom
newskipped = (skipped[0]+[first[0]], skipped[1])
result += res._iterate_first(first[1:], second, bindings, used, newskipped, finalize_method, debug+1)
try:
newbindings, newused, unused = res._unify_terms(first[0], second[0], bindings, used)
#Unification found, so progress with this line of unification
#put skipped and unused terms back into play for later unification.
newfirst = first[1:] + skipped[0] + unused[0]
newsecond = second[1:] + skipped[1] + unused[1]
# We return immediately when `_unify_term()` is successful
result += _simplify(finalize_method(newfirst,newsecond,newbindings,newused,([],[]),debug))
except res.BindingException:
pass
return result
res._iterate_first=_iterate_first_fix
Similarly update res._iterate_second
def _iterate_second_fix(first, second, bindings, used, skipped, finalize_method, debug):
"""
This method facilitates movement through the terms of 'other'
"""
debug.line('unify(%s,%s) %s'%(first, second, bindings))
if not len(first) or not len(second): #if no more recursions can be performed
return finalize_method(first, second, bindings, used, skipped, debug)
else:
#skip this possible pairing and move to the next
newskipped = (skipped[0], skipped[1]+[second[0]])
result = res._iterate_second(first, second[1:], bindings, used, newskipped, finalize_method, debug+1)
try:
newbindings, newused, unused = res._unify_terms(first[0], second[0], bindings, used)
#Unification found, so progress with this line of unification
#put skipped and unused terms back into play for later unification.
newfirst = first[1:] + skipped[0] + unused[0]
newsecond = second[1:] + skipped[1] + unused[1]
# We return immediately when `_unify_term()` is successful
result += _simplify(finalize_method(newfirst,newsecond,newbindings,newused,([],[]),debug))
except res.BindingException:
#the atoms could not be unified,
pass
return result
res._iterate_second=_iterate_second_fix
Finally, plug our function into the clausify() to ensure the inputs are repetition-free.
def clausify_simplify(expression):
"""
Skolemize, clausify, and standardize the variables apart.
"""
clause_list = []
for clause in res._clausify(res.skolemize(expression)):
for free in clause.free():
if res.is_indvar(free.name):
newvar = res.VariableExpression(res.unique_variable())
clause = clause.replace(free, newvar)
clause_list.append(_simplify(clause))
return clause_list
res.clausify=clausify_simplify
After applying these changes the prover should run the standard tests and also deal correctly with the parentof/childof relationships.
print res.ResolutionProver().prove(q, [s], verbose=True)
output:
[1] {-foo(Bar)} A
[2] {-parentof(z144,z143), childof(z143,z144)} A
[3] {parentof(z146,z145), -childof(z145,z146)} A
[4] {childof(z145,z146), -childof(z145,z146)} (2, 3) Tautology
[5] {-parentof(z146,z145), parentof(z146,z145)} (2, 3) Tautology
[6] {childof(z145,z146), -childof(z145,z146)} (2, 3) Tautology
False
Update: Achieving correctness is not the end of the story. A more efficient solution would be to replace the container used to store literals in the Clause class with the one based on built-in Python hash-based sets, however that seems to require a more thorough rework of the prover implementation and introducing some performance testing infrastructure as well.