Understanding "saturating" theorem provers

Question

The documentation for the E Theorem Prover explains this as the first step in its process:

A clausification algorithm translates first-order input into clause normal form, such that the resulting formula is unsatisfiable if and only of the original problem is provable.

Does this simply mean that it will attempt to find a proof by contradiction (using CNF)? Or is this a more complicated process, using some other mechanism to prove the objective?

If so, is this done because it's easier to search for contradictions than to search for direct proofs?

Answer 1

The basic idea is we want to check if a formula $\varphi$ is satisfiable. This is analogous to checking there exists a row in the truth-table for a proposition for which the proposition is true. First-order logic is not as simple as "write down the truth-table", because it requires constructing a model and an interpretation.

Recall, there are three related notions:

1. Unsatisfiability means there is no interpretation for which $\varphi$ holds
2. Validity means $\varphi$ holds in every interpretation
3. Satisfiability means there is at least one interpretation for which $\varphi$ holds.

A common trick to proving $\varphi$ is satisfiable is to try to prove its negation $\neg\varphi$ is unsatisfiable.

Another common trick is to transform our formula $\varphi$ into an equisatisfiable form like conjunctive normal form. Conjunctive normal form is useful for proving a formula is valid...but if $\neg\varphi$ is valid, then $\varphi$ is unsatisfiable. So we want to prove $\neg\varphi$ is not valid, which can be done quickly and efficiently.

For a detailed walkthrough about this process, John Harrison's Handbook of Practical Logic and Automated Reasoning discusses this in chapter 2, section 6 et seq.