# Is there a standard definition of resolution for arbitrary clauses?

Knuth defines in [1] a resolution operator for arbitrary clauses which sets $$C = C' \diamond C'' = (C' \lor C'')$$ when there is no literal $$x$$ such that $$x \in C'$$ and $$\neg x \in C''$$. I skimmed over [2], [3] and [4] and could not find any references to this particular style.

Why is this definition sensible for general clauses? How is it different from, say, defining $$C = C' \diamond C'' = \top$$, a tautology, in such case?

[1] Knuth, TAOCP, Volume 4 Fascicle 6, Satisfiability

[3] Buss, Samuel R. (ed.), Handbook of proof theory, Studies in Logic and the Foundations of Mathematics. 137. Amsterdam: Elsevier. 811 p. (1998). ZBL0898.03001.

[4] Krajíček, Jan, Proof complexity, ZBL07044161.

• I'd need to read up on the diamond operator but certainly removing multiple literals and their negations does not work - after all ¬A ∨ ¬B ≠ ¬(A ∨ B). Perhaps resolution is defined differently then? – lambda.xy.x Apr 16 at 7:53
• And perhaps another rather obvious observation: the cut rule can be seen as resolution on general formulas (the unifying substitution has to be handled differently though). – lambda.xy.x Apr 16 at 8:25