For an assignment we had to write Python code that performs resolution on a propositional logic KB.
All code seems to work fine, except for the recursive_print_proof. When running the program, it will keep running until you tell it to stop.
What it should do is output a proof, based on the resolution. However, it seems to get stuck in a loop.
Hopefully anyone can help me.
recursive_print_proof can be found almost at the end. My code is:
def recursive_print_proof(idx, clause_set):
kb = init()
if contains_empty_clause(kb):
inferred = []
for i in range(len(kb)):
for j in range(i,len(kb)):
if can_resolve(kb[i],kb[j]):
resolvent = resolve_clauses(kb[i],kb[j])
inferred.append(resolvent)
if clause_set[idx].equals(resolvent):
idx2 = find_index_of_clause(kb[j],clause_set)
recursive_print_proof(idx2,clause_set)
idx2 = find_index_of_clause(kb[i],clause_set)
recursive_print_proof(idx2,clause_set)
# printing
clause_set[idx].print_clause()
print(" is inferred from", end=" ")
kb[i].print_clause()
print(" and", end=" ")
kb[j].print_clause()
print(".")
break
break
break
If you want to know why the code is spinning in recursive_print_proof...
your recursive_print_proof method loops on a condition while not contains_empty_clause(kb): which will never be false. So it keeps spinning.
Perhaps you want it to be if not contains_empty_clause(kb): ?