Untitled
unknown
plain_text
a year ago
881 B
2
Indexable
def pl_resolution(kb, alpha): clauses = kb + [negate(alpha)] new = set() while True: n = len(clauses) for i in range(n): for j in range(i + 1, n): resolvents = resolve(clauses[i], clauses[j]) if [] in resolvents: return True new.update(resolvents) if new.issubset(set(clauses)): return False clauses.extend(new) def resolve(ci, cj): resolvents = [] for di in ci: for dj in cj: if di == negate(dj): resolvent = set(ci).union(set(cj)) resolvent.remove(di) resolvent.remove(dj) resolvents.append(list(resolvent)) return resolvents def negate(literal): if literal.startswith('~'): return literal[1:] else: return '~' + literal
Editor is loading...
Leave a Comment