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.
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.Sign up to join this community
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.