Resolution and proof by refutation
Resolution is an inference rule that works on clauses, which are disjunctions of literals (a symbol or its negation) such as ¬P ∨ Q. Any propositional sentence can be converted to conjunctive normal form, a conjunction of clauses, by eliminating implications, moving negations inward, and distributing or over and. Given two clauses that contain a literal and its complement, resolution produces a new clause containing all the remaining literals of both.
Python
from itertools import combinations
def negate(literal):
return literal[1:] if literal.startswith("~") else "~" + literal
def resolve(first, second):
return [(first - {lit}) | (second - {negate(lit)}) for lit in first if negate(lit) in second]
def refutes(clauses):
clauses = set(clauses)
while True:
new = set()
for first, second in combinations(clauses, 2):
for resolvent in resolve(first, second):
if not resolvent:
return True
new.add(frozenset(resolvent))
if new <= clauses:
return False
clauses |= new
kb = [frozenset({"~P", "Q"}), frozenset({"~Q", "R"}), frozenset({"P"})]
print(refutes(kb + [frozenset({"~R"})]))
print(refutes(kb + [frozenset({"~S"})]))