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

[2] https://en.wikipedia.org/wiki/Resolution_(logic)

[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.

  • $\begingroup$ 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? $\endgroup$ – lambda.xy.x Apr 16 at 7:53
  • $\begingroup$ 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). $\endgroup$ – lambda.xy.x Apr 16 at 8:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.