# What were the shortcomings of Robinson's resolution procedure?

Paulson et alii. From LCF to Isabelle/HOL say:

Resolution for first-order logic, complete in principle but frequently disappointing in practice.

I think complete means they can proof any true formula in first-order logic correct. In the Handbook of Automated Reasoning I find:

Resolution is a refutationally complete theorem proving method: a contradiction (i.e., the empty clause) can be deduced from any unsatisfiable set of clauses.

From Wikipedia:

Attempting to prove a satisfiable first-order formula as unsatisfiable may result in a nonterminating computation

Why is that disappointing?

• Suppose you run the procedure on a statement and it's still running after two weeks. What have you learned about the statement? Aug 16 '20 at 16:41

A famous example is an encoding of the pigeon hole principle for $$n$$ holes in propositional logic (which is the statement "$$n+1$$ pigeons cannot fit in $$n$$ holes without duplicates). There is no proof of this statement using only resolution in time sub-exponential in $$n$$.