I'm searching for an authoritative definition of resolution (logic resolution).

Preferably on a reference freely available on the Internet (so I can read it right now).

If this is too broad then resolution for first order logic.

Thank you.

  • 2
    $\begingroup$ Too basic for this site. $\endgroup$ Aug 8, 2013 at 19:10
  • 3
    $\begingroup$ Try googling "resolution proof system". $\endgroup$ Aug 8, 2013 at 19:11
  • 1
    $\begingroup$ @YuvalFilmus I think you didn't understand the question, please let me know any detail that may not be clear. Thank you. $\endgroup$
    – Trylks
    Aug 9, 2013 at 10:31
  • 1
    $\begingroup$ @Trylks, he wikipedia articles for resolution en.wikipedia.org/wiki/Resolution_(logic) and inference rules explain all these topics. Do you want a definition of resolution or to know whether it has certain properties? Your context does not help because both statements about resolution are vague. I don't understand the focus on "new theorems". $\endgroup$
    – Vijay D
    Aug 10, 2013 at 0:23
  • 1
    $\begingroup$ See also this discussion: cstheory.stackexchange.com/questions/16572/… $\endgroup$
    – Vijay D
    Aug 10, 2013 at 0:26

1 Answer 1


Unlike the question you threaten for inference rule, this has a nice, simple answer:

Robinson (1965) A machine-oriented logic based on the resolution principle. Journal of the ACM.

Resolution only applies to a subfragment of FOL, the Horn clauses, that lack disjunction and existential quantification, but combined with Herbrandisation, this is sufficient to encode satisfiability in the following sense: for any formula of FOL, we can find a Horn clause such that each is satisfiable if the other is.

Resolution is related to cut-elimination, but is more efficient.

Extending resolution to the whole of FOL requires a more sophistcated approach to unification than Robinson's algorithm. Uniform provability offers a technique for reading off such a computational mechanism from a cleaned-up proof theory of intuitionistic logic, higher-order unification, and the double-negation translation.


Not the answer you're looking for? Browse other questions tagged or ask your own question.