What is resolution ((in FOL))? 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.
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.