Note II Independent explainer
How a first order logic theorem prover works
Provers rarely work on formulas as people write them. They convert them to a rigid clause form first, and each conversion step has a reason.
What first-order logic adds
Propositional logic talks about whole statements joined by and, or and not. First-order logic adds objects, functions, predicates and the quantifiers for all and there exists. That is enough to state most of ordinary mathematics, which is why it is the standard target for automated theorem proving.
The extra power has a price. Gödel's completeness theorem, from 1929 to 1930, shows that every valid first-order sentence has a proof. In 1936 Church and Turing independently showed that no algorithm can decide validity for every sentence. First-order validity is therefore semi-decidable: a prover can eventually confirm a valid sentence, but on some invalid ones it may run forever.
From formula to clauses
Before resolution can start, the input is normalised. The usual steps are listed below, and each one preserves what matters for the proof.
First, remove implications and equivalences. Second, push negations inward until they sit on atoms. Third, rename bound variables so that no two quantifiers share a name. Fourth, remove existential quantifiers by Skolemization. Fifth, drop the remaining universal quantifiers and treat all variables as universal. Sixth, distribute or over and so the formula becomes a conjunction of clauses.
A Skolemization example in plain words
Take the sentence that for every x there is a y with Loves(x, y). Skolemization replaces y by a new function symbol applied to x, giving Loves(x, f(x)). The function stands for the witness that the existential quantifier promised.
The result is not logically equivalent to the original, but it is satisfiable exactly when the original is. That is all a refutation proof needs, because the prover only asks whether the clause set is satisfiable.
Herbrand's idea
Jacques Herbrand's work around 1930 shows that an unsatisfiable set of clauses has a finite unsatisfiable set of ground instances, that is, instances with no variables. This reduces first-order reasoning to a search over propositional-like problems, and it is the theoretical root of resolution and of many later methods.
Equality needs special care
Equality can be axiomatised with a handful of clauses, but doing so produces a huge search space. Provers instead treat equality with dedicated rules. Paramodulation, introduced in 1969, and later superposition let a prover rewrite one term into another directly. Problems that consist only of equations form a division of their own in competitions.