1929
Completeness of first-order logic
Gödel's doctoral work, published in 1930, shows that every valid first-order sentence has a proof. A systematic search will therefore find that proof eventually.
Read about the logic
Independent explainer / Logic / Automated reasoning
Automated theorem proving: how machines prove by cancelling contradictions
A plain-language guide to automated theorem proving: resolution, first-order logic, the TPTP format, the CASC competition, SAT and SMT solvers, and proof assistants. Scroll to watch a field of clauses cancel down to nothing.
The idea
Prove it by showing the opposite is impossible
Automated theorem proving is the study of programs that decide, without human steps, whether a statement follows from a set of assumptions. The best-known approach, resolution, does not build the proof directly. It adds the negation of the goal to the assumptions and searches for a contradiction.
When two clauses contain a literal and its negation, the rule cancels the pair and merges what is left. If the cancelling ends in a clause with nothing left, the assumptions and the negated goal cannot all be true, so the goal holds. The full explanation takes five minutes to read.
- Literal
- An atomic statement such as human(socrates), or its negation.
- Clause
- A set of literals joined by or. A clause set means all of them hold together.
- Unifier
- A substitution that makes two literals identical, for example X replaced by socrates.
- Empty clause
- A clause with no literals. It cannot be true, so deriving it proves the set contradictory.
Step by step
A refutation in five lines
The classic example: all humans are mortal, Socrates is human, so is Socrates mortal? Scroll to run the proof.
- 1
~human(X) | mortal(X)Premise: every human is mortal - 2
human(socrates)Premise: Socrates is human - 3
~mortal(socrates)Negated goal: assume Socrates is not mortal - 4
mortal(socrates)Resolve 1 and 2, with X replaced by socrates - 5
Resolve 3 and 4: nothing is left, so the goal is proved
Contradiction reached. The goal follows from the premises.
Eight milestones
From completeness to competitions
Scroll sideways through the dates that shaped the field. Each card links to a guide.
A shared language
The same proof, written for a prover
Provers from different groups read one plain-text format, TPTP. Each line is an annotated formula: a language, a name, a role and the formula itself.
foffirst-order formula, withcnffor clausesaxioma premise,conjecturethe goal to prove![X]:for all X,=>implies,~not
% Socrates, written in TPTP
fof(humans_are_mortal, axiom, ![X]: (human(X) => mortal(X))).
fof(socrates_is_human, axiom, human(socrates)).
fof(socrates_is_mortal, conjecture, mortal(socrates)).
% SZS status Theorem for socratesHow the ideas connect
A map of the terms in these guides
Fourteen terms from this site, joined by relations the guides state. For example, Skolemization is one step of turning a formula into clauses, and TPTP is the format CASC problems are written in. Drag to turn the map, hover a point to read its name, click to open the guide.
Guides
- ResolutionWorks on clauses and ends when the empty clause is derived.
- First-order logicTurns a formula into clauses before resolution can start.
- TPTP formatWrites problems as annotated formulas, with cnf for clauses.
- CASCGives every competing system problems written in TPTP.
- SAT and SMTCompares propositional solvers with first-order provers.
- Proof assistantsA person writes the proof and the system checks it.
Terms
- ClauseA set of literals joined by or, the form resolution works on.
- UnificationMakes two literals identical so a clashing pair can be cancelled.
- Empty clauseDeriving it shows the clause set is contradictory.
- SkolemizationOne normalisation step, it removes existential quantifiers.
- Herbrand's ideaReduces first-order reasoning to ground instances, a root of resolution.
- Equality rulesParamodulation and superposition rewrite terms without huge axiom sets.
- SMT solverSAT plus theories, such as arithmetic.
- HammerA tool inside a proof assistant that sends goals to external provers and SMT solvers.
The reading list
Six guides to read in any order
- Resolution, explainedThe rule, the empty clause and why proving by contradiction suits a machine.
- First order logic theorem proversQuantifiers, semi-decidability and the steps that turn a formula into clauses.
- The TPTP format and syntaxAnnotated formulas, roles, operators and the status words provers print.
- The CASC prover competitionWho competes, what they solve, how the winner is chosen and what it means.
- SAT, SMT and first-order proversWhat each tool class decides, where it is fast and how they cooperate.
- Proof assistants and automated proversInteractive and automatic tools compared, with the hammer that connects them.
Quick answers
Questions newcomers ask
- Can a computer prove any true statement?
- No. For first-order logic no algorithm can decide every statement, so provers may run forever on some inputs. See first-order logic for provers.
- What is the difference between a SAT solver and a theorem prover?
- A SAT solver handles propositional formulas and is very fast, while a first-order prover handles quantifiers and is far more general. The comparison page explains when to use which.
- What does a prover competition measure?
- Fully automatic systems are run on the same problems under a fixed time limit and ranked by how many they solve. Read how CASC works and what its results do not show.
- Can AI prove theorems?
- Language-model systems now attempt formal proofs, but the result is only accepted when a proof assistant such as Lean checks it step by step. The checker, not the AI, decides whether a proof is valid. See proof assistants and automatic provers.
- Are proof assistants the same as automatic provers?
- No. In a proof assistant a person writes the proof and the system checks it, although tools called hammers can call automatic provers. See the comparison.