Untitled

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