Pravda - resolution
Resolution in propositional logic
Resolution rule: special case modus ponens
not p or q * p * //q
Resolution rule: general case
not s or not p or q or r* q or p or t * //not s or q or r or t
A small refutation proof
not p or not q or r * not r * not p or q * p * //not p or not q //not p //bottom
Resolution in first-order logic
Resolution rule
P(x) * not P(x) or Q(x) * //Q(x)
P(a) * not P(x) or Q(x) * //Q(a)
Contraction rule
P(a) or P(x) or Q(x) * //P(a) or Q(a)
Refutation proofs
P(x) or not P(f(x)) * not P(a) * P(f(f(a))) * //not P(f(a)) //not P(f(f(a))) //bottom
R(x,y) or R(f(x),x) * R(x,y) or R(x,f(x)) * not R(x,y) or not R(y,z) or R(x,z) * not R(x,x) * //R(f(x),x) //R(x,f(x)) //not R(z,f(x)) or R(z,x) //R(x,x) //bottom
R(f(y), a) or R(f(y), y) * not R(x, a) or R(x, x) * not R(v, f(y)) or not R(v, y) * //R(f(a), a) //not R(f(y), a) or not R(f(y), y) //not R(f(a), a) //bottom
not P(x) or Q(f(x),x) * not P(x) or not Q(y,x) or R(y) * not R(y) or not S(y) or not P(x) or not Q(y,x) * not S(y) or R(y) * P(a) * not R(x) or S(x) * //not R(y) or not P(x) or not Q(y,x) //not P(x) or not Q(y,x) or not P(z) or not Q(y,z) //not P(x) or not Q(y,x) //not P(x) //bottom