The unit of inference no longer has to fit one human glance
Robinson begins with an engineering premise disguised as a philosophical one: the traditional size of an inference step reflects the limits of its human checker. A computer can reliably execute a more complicated, more informative primitive.
Classical calculi decompose reasoning into small moves because a person must recognise each move as correct. That discipline makes a written proof inspectable, but it is not a law of logic. If a program checks the rule mechanically, one application may perform substantial combinatorial work while remaining exactly specified. Robinson calls his rule machine-oriented in this limited and concrete sense.
The resolution principle combines two operations which earlier proof procedures alternated. First, those procedures generated many ground instances by substituting terms for variables. Then they applied truth-functional analysis to the enlarged propositional set. The alternation is complete, yet its intermediate Herbrand expansions can become enormous before the decisive instances appear.
Resolution moves the choice of substitution inside the inference. It asks whether literals from two clauses can be made complementary, computes their most general common instance, and immediately derives the consequence that remains when the complementary pair is removed. A useful term is generated because a particular inference demands it, not because its level in a universal enumeration has arrived.
This is not an assertion that large rules are intrinsically intelligent. The rule is a deterministic symbolic operation, and its power depends on representation, clause selection and a search policy. The paper's achievement is narrower and stronger: one precisely defined rule forms a complete refutation system for first-order logic, and its substitutions double as an economical route through the otherwise vast instance space.
Worked example · one move can contain many replacements
To compare P(x, f(y), y) with P(g(a), f(b), b), a machine may discover x↦g(a) and y↦b together. A human-oriented calculus might expose those replacements as separate steps; resolution packages the verified composition into the inference that needs it.
Causal probe · force single-variable steps
Require every inference to change only one variable. Correctness need not disappear, but the search gains many intermediate states and many orders for making the same substitutions. The smaller rule can create a larger control problem.
A theorem becomes an attempt to derive the empty clause
The paper organises logic around unsatisfiability and refutation rather than validity and direct proof. This change gives the machine a single, unmistakable terminal object: the empty clause.
A clause is a finite set of literals. A literal is an atomic formula or its negation. Order and repetition inside a clause do not matter, because the clause denotes a disjunction. Its variables are implicitly universally quantified. A finite set of clauses denotes their conjunction. The empty clause contains no literal that could make it true, so any set containing it is unsatisfiable.
To prove a target, negate it and transform the result into clause form. Existential variables are removed by Skolem functions or constants; universal prefixes can then be omitted. Robinson takes this special form as the input language. The transformation work is logically important, but the paper's central theory starts after a finite set of clauses has been produced.
The distinction between the empty set of clauses and the empty clause is essential. The empty set has no constraints and is satisfiable. The empty clause is a constraint with no satisfying literal and is false under every interpretation. Confusing the two would reverse the meaning of both successful simplification and successful refutation.
Ground clauses contain no variables. For two ground clauses, choose a complementary pair L and ¬L, remove them, and unite what remains. The result is a ground resolvent. Any model of both parents is a model of that resolvent: if L is false, the first parent's residue must be true; if L is true, the second parent's residue must be true. Resolution therefore preserves semantic consequence.
Worked example · the final cancellation
Resolve {P(a)} with {¬P(a)}. Deleting the complementary singletons leaves no literals, so the resolvent is □. The input pair cannot have a model, and the derived empty clause records that fact without depending on a separate truth table.
Causal probe · confuse no clauses with an empty clause
Deleting every satisfied constraint leaves ∅, which means success for a model search. Deriving □ means failure for every model. A representation that assigns both states the same empty container cannot implement the proof contract correctly.
Herbrand saturation is complete and combinatorially indiscriminate
Robinson does not reject Herbrand's theorem. He uses it as the bridge that proves resolution complete, while showing why a literal implementation of saturation spends effort in the wrong order.
The Herbrand universe of a clause set contains the ground terms buildable from its function symbols, adding a constant if none occurs. Saturating a clause over a finite term set means replacing its variables with every permitted combination of those terms. Herbrand's theorem says that an unsatisfiable finite clause set has some finite unsatisfiable collection of such ground instances.
A level-saturation procedure enumerates progressively deeper terms H₀, H₁, H₂ and tests each growing propositional expansion. It is fair: if a finite proof set exists, some level eventually contains it. Yet the number of terms can grow explosively with function arity and depth, and a clause with several variables multiplies that term count across argument positions.
The primary imagines a benevolent “proof set demon” which hands the program exactly the small set of ground terms needed for the contradiction. Earlier work could approximate that demon with guidance from a mathematician. The challenge is to make relevance a computation. Resolution approaches this goal because unification constructs terms as a by-product of matching the inference's pivot.
Fairness and focus are different virtues. Blind saturation is fair but unfocused. A resolution search can be focused but, depending on its clause-selection policy, may still follow an infinite irrelevant chain. Completeness of the calculus means a refutation exists and a suitable systematic enumeration can find it; it does not mean every practical strategy terminates quickly or at all.
Worked example · depth becomes a Cartesian product
If a level holds 100 terms and a clause has four distinct variables, naive saturation offers up to 100⁴ substitutions before duplicate removal. A contradiction needing only x↦f(a) can be hidden inside one hundred million candidates.
Causal probe · give the demon the proof set
Supply only the few ground terms used in a refutation. The propositional stage becomes small, showing that first-order undecidability is not the only obstacle. Much practical waste lies in finding relevant instances rather than checking the finite contradiction once found.
Unification starts at the first place expressions disagree
The unification algorithm converts structural mismatch into a sequence of substitutions. It either reaches one common expression or halts when the disagreement cannot be repaired.
Take a finite set of expressions and scan them in parallel. If they are already identical, the current substitution is a unifier. Otherwise locate the first symbol position at which they differ and form the disagreement set from the subexpressions beginning there. A repair is possible when that set contains a variable V and another term U in which V does not occur. Substitute U for V everywhere and repeat.
The “does not occur” condition is now called the occurs-check. Without it, trying to solve x=f(x) would create an infinite self-reference rather than a finite first-order term. Robinson's algorithm therefore halts in failure if a disagreement set lacks a permissible variable-term pair. Distinct function or predicate symbols at the same position are a direct structural clash.
Substitutions compose. If the first repair is x↦y and the second is y↦a, the composition must also update x to a. Treating the components as an unordered list of one-time textual replacements can leave a supposedly unified pair unequal. The paper defines composition so instantiating by the composition has exactly the effect of applying its constituent substitutions in sequence.
The algorithm's output is a most general unifier. “General” means it makes no commitment beyond equality: any other unifier can be obtained by applying some further substitution to the most general one. Renaming variables may produce an equivalent answer. The key property is factorisation, not the spelling or order of substitution components.
Worked example · generality leaves z open
The pair above does not require a value for z. Setting z↦b would also unify it, but that answer is less general. The MGU retains z as a parameter, allowing the derived resolvent to stand for every later instance.
Causal probe · omit the occurs-check
Accept x↦f(x) while unifying P(x) and P(f(x)). Reapplying the substitution produces f(f(x)), then f(f(f(x))), never equal finite terms. A tiny local omission turns termination and sound term representation into an unbounded structure.
Identical variable names in different clauses must not imply identity
Before resolving two clauses, Robinson gives their variables separate alphabets. This administrative step prevents accidental constraints that are not licensed by universal quantification.
Variables in different universally quantified clauses are local placeholders. The x in P(x)∨R(x) and the x in ¬P(f(x))∨S(x) need not denote the same individual in an inference. If a program merges them before unification, it may demand x=f(x), fail the occurs-check and miss a valid resolvent.
Robinson defines x-standardisation and y-standardisation: systematically rename every variable of the first parent to x₁, x₂ and so on, and every variable of the second to y₁, y₂ and so on. The renamed clauses are variants of their parents. Their disjoint variable sets make every later equality an explicit product of unification rather than a collision in the parser.
With C={P(x),R(x)} and D={¬P(f(x)),S(x)}, standardise them as {P(x₁),R(x₁)} and {¬P(f(y₁)),S(y₁)}. The pivots unify by x₁↦f(y₁). The resolvent is {R(f(y₁)),S(y₁)}. It remains universally quantified and represents every ground instance of that relation.
Freshness is an invariant across repeated inferences. It is not enough to standardise a source file once, because a derived clause may later meet another variant of itself or an ancestor. Implementations typically rename variables on clause retrieval or attach unique identifiers. The principle is the same: variable scope belongs to a clause occurrence, not merely to a printed letter.
Worked example · a false failure repaired
Without renaming, P(x) and ¬P(f(x)) seem to require the forbidden equation x=f(x). After standardising apart, P(x₁) and ¬P(f(y₁)) unify immediately. Fresh names expose the legal relationship between two independent universal instances.
Causal probe · share variables across parents
Resolve clauses exactly as parsed, retaining their coincident names. Some sound inferences vanish and others acquire unintended dependencies. The calculus has not changed; the implementation has silently changed variable scope.
Unification manufactures the complementary ground pattern on demand
A first-order resolvent is not obtained by cancelling literals as printed. The machine first asks whether selected literals can become one complementary pattern under their most general unifier.
For two clauses C and D, standardise C with x-variables and D with y-variables. Select a non-empty subset L of the first and M of the second. Strip negation from the selected literals and ask whether the resulting atoms are most generally unifiable, with the polarities arranged so every selected literal from one side becomes complementary to every selected literal from the other.
Robinson calls the selection together with its unifiable atomic set a key triple. Apply the MGU to both standardised parents, remove the selected literals and unite the remainder. Because several selected literals may collapse to one after substitution, the definition incorporates what later presentations often separate as factoring. It can delete duplicate instances within a parent while resolving across parents.
The familiar binary form is the simplest case. From {P(x),R(x)} and {¬P(f(y)),S(y)}, select only P(x) and ¬P(f(y)). Their atoms have MGU x↦f(y). Removing the pivot and applying that substitution yields {R(f(y)),S(y)}. This clause is a consequence of the parents and stands for all its ground instances.
Two clauses can have no resolvent, one resolvent or several resolvents, depending on which complementary-looking subsets unify. The set is nevertheless finite because each parent has finitely many literals and each finite selected atom set has at most the relevant most general unifier up to variable renaming. Search must decide which finite opportunity to take next.
Worked example · a symbolic child covers infinitely many ground children
The resolvent {R(f(y)),S(y)} covers y↦a, y↦f(a), y↦f(f(a)) and every other ground term. One first-order inference represents a family that level saturation would enumerate member by member.
Causal probe · ground both parents first
Choose a finite term level, instantiate x and y exhaustively, then resolve complementary ground literals. Each derived clause is valid, but the single symbolic relation fragments into many instances and may require a much deeper level before the useful pair is present.
Resolution semi-commutes with saturation
The paper's decisive proof bridge says that resolving after grounding produces nothing essentially unavailable by resolving first and grounding afterwards.
Let P be a subset of the Herbrand universe and P(S) the ground saturation of clause set S over P. A ground resolvent of two instances from P(S) depends on some substitution that made their selected literals complementary. By the Unification Theorem, that substitution factors through the most general unifier used by a first-order resolvent of the original clauses.
Therefore every clause obtained by one ground-resolution step after saturation belongs to the saturation of the first-order resolution: R(P(S)) ⊆ P(R(S)). Robinson describes this as semi-commutativity. The inclusion need not go in the reverse direction, because first-order resolution may construct terms not available in the chosen finite P.
Iterating the lemma gives the corresponding inclusion for any finite number of resolution rounds. The order of operations can be reversed: instead of expanding terms first and resolving later, resolve clauses symbolically first and regard grounding as postponed. Crucially, substitution cannot turn a non-empty clause into the empty clause. If the saturated side reaches □, the symbolic side must already contain □.
This argument transfers the Ground Resolution Theorem to the first-order system. Herbrand's theorem supplies a finite unsatisfiable ground core; ground resolution derives the empty clause from it; semi-commutativity lifts those steps to symbolic resolution; and emptiness cannot be an artefact of later instantiation. The proof does not abandon the old completeness machinery. It reorders it.
Worked example · factor an arbitrary ground match through the MGU
Suppose a ground inference used x↦f(a) and y↦a to match P(x) with P(f(y)). The MGU is x↦f(y); applying y↦a afterwards reproduces the ground substitution. The symbolic resolvent is therefore general enough to generate the exact ground child.
Causal probe · demand equality instead of inclusion
For a small term set P, resolving first may create a clause whose useful instance requires a term outside P. P(R(S)) can therefore contain more than R(P(S)). The one-way inclusion is sufficient for completeness and is the precise claim.
An unsatisfiable finite clause set has a finite resolution refutation
The Resolution Theorem states the exact success condition: S is unsatisfiable if and only if some finite iteration of resolution contains the empty clause.
Soundness runs forward. Each resolvent is entailed by its parents, so deriving □ from S is impossible when S has a model. Completeness runs backward through the bridge just described. If S is unsatisfiable, Herbrand's theorem exposes a finite unsatisfiable ground fragment, ground resolution reaches □, and the semi-commutativity argument guarantees that some finite symbolic resolution level contains □.
A refutation is a finite sequence of clauses. Each member is either an original premise or a resolvent of two earlier members, and the last is □. This sequence is a checkable certificate: a verifier need not repeat the search, only standardise parents, recompute each MGU, validate each resolvent and confirm the empty final clause.
The simplest procedure repeatedly adds every resolvent of every pair until it sees □ or reaches a fixed point. For finite ground inputs, only finitely many clauses can be formed from the existing ground literals, so saturation terminates. For first-order inputs, new terms and ever longer clauses can arise without bound. Church's theorem rules out a terminating decision procedure for all cases.
Semi-decision is therefore the honest contract. With a fair enumeration, unsatisfiable inputs eventually produce a refutation. A satisfiable input may stabilise in favourable cases, or the process may continue indefinitely. Completeness guarantees the existence and discoverability of positive certificates under fairness; it does not supply a general negative stopping rule.
Worked example · a three-line refutation
Let C₁={P(x)}, C₂={¬P(y),Q(y)} and C₃={¬Q(a)}. Resolve C₁ with C₂ using x↦y to derive {Q(y)}. Resolve that clause with C₃ using y↦a and obtain □. The substitutions select exactly the ground path needed.
Causal probe · stop after a quiet round
A scheduler that examines only some clause pairs may complete a round without a new clause even though unvisited pairs have useful resolvents. “No result from this policy” is not a fixed point of the calculus. A satisfiable verdict requires stronger closure conditions than a temporary lull.
Large machine steps can compress a remote contradiction
Robinson's second worked refutation formalises an associative system with left and right solutions and denies the existence of a right identity. A short resolution sequence reaches contradiction.
The example uses Q(x,y,z) for an equation formed by the system's binary operation. Clauses encode associativity, the existence of left and right solutions, closure and the denial of a right identity. Several literals and variables must line up across an inference. The resulting most general unifier contains nested terms that would occur very deep in a level-by-level Herbrand universe.
The paper reports that a relevant proof set first appears at a level whose scale is beyond a feasible saturation procedure. Resolution instead computes the needed nested terms as components of its unifier. What looked like a supernatural proof-set oracle becomes a deterministic consequence of trying to make selected atoms agree.
The refutation is compact enough that two associativity clauses are not used. That detail distinguishes the logical certificate from the original encoding. A proof can reveal which premises were dispensable for this derivation. It does not establish that those premises are irrelevant to every formulation or every intended algebraic interpretation.
Robinson notes that a resolution step may exceed what a person can apprehend in one intellectual act. Inspectability is recovered by algorithmic replay: run the unification algorithm, check the transformed pivots, and verify the residue. The inference is psychologically large but formally decomposable, which is precisely the machine-oriented bargain.
Worked example · term discovery is evidence discovery
A nested substitution such as x↦f(g(y),h(y)) is not guessed as an isolated object. It appears because the outer symbols and arguments of two pivot atoms must agree. Each disagreement constrains the next repair, turning term construction into a traceable causal sequence.
Causal probe · bound term depth below the required nest
A level-saturation prover can remain perfectly correct yet never expose the decisive instance within its resource budget. The resolution refutation may still reach it because depth is paid only along the selected pivot, not across every term combination of the same level.
Completeness defines the space; search engineering decides whether it is usable
The final section refuses to confuse a complete rule with an efficient prover. Robinson introduces purity, subsumption and replacement as transformations of the search state.
A raw procedure that adds all resolvents can generate an infinite harmless chain. From {Q(a)} and {¬Q(x),Q(f(x))}, it derives Q(f(a)), Q(f(f(a))) and so on. The literal Q(f(x)) in the second clause is pure relative to the set in Robinson's formal sense: it has no possible complementary key triple with another clause. The purity principle permits deleting a clause containing such a literal while preserving satisfiability.
Subsumption removes a weaker, more specific clause. C subsumes D when some instance Cσ is a subset of D. For example, {P(x)} subsumes {P(a),R(a)}. Any model satisfying all instances of the first already satisfies the second, so retaining D adds search weight without adding constraint. Robinson supplies a terminating algorithm for deciding the relation.
Replacement combines inference and deletion. If a new resolvent subsumes one of its parents, add the child and remove that parent. The clause set either has fewer clauses or a clause with fewer literals. This turns a potentially inflationary inference step into a measurable simplification.
These are search principles rather than inference principles because they govern which equivalent satisfiability problem to keep, not which logical consequence may be derived. Applying them to exhaustion produces an irreducible state before new resolution steps are admitted. The distinction anticipates a durable architecture: a sound calculus generates possibilities, while redundancy control and scheduling determine resource use.
Worked example · subsumption as semantic garbage collection
Keep C={P(x)} and D={P(a),R(a)}. With σ={x↦a}, Cσ={P(a)}⊂D. Deleting D loses no model restriction supplied by C, while avoiding future pairings involving an extra literal and a fixed constant.
Causal probe · delete by clause length alone
A short clause is often stronger, but length does not prove subsumption. Deleting {P(a),Q(a)} merely because {P(x),R(x)} is shorter can change satisfiability. The safe reduction requires an explicit substitution and subset test.
Unify a pivot, inspect the substitution, and audit the resolvent
Five controls each choose one first-order resolution job. Together they define 4⁵=1,024 laboratory configurations. The page recomputes all of them and checks successful MGUs, resolvents and occurs-check failures.
Running MGU audit…
Running resolvent audit…
Running occurs-check audit…
Worked example · default job one
The positive parent is P(x,a)∨R(x); the negative parent is ¬P(b,y)∨S(y). The disagreements x versus b and a versus y yield {x↦b,y↦a}. After deleting the unified pivots, the displayed resolvent is R(b)∨S(a).
Causal probe · choose the cyclic pair
Select P(x) against ¬P(f(x)). The trace reaches x versus f(x) and rejects the binding because x occurs inside its proposed replacement. No resolvent is emitted; failure is a structural result, not an arbitrary timeout.
Claims, conditions and audit handles
| Claim | Condition | Audit handle |
|---|---|---|
| A first-order resolvent is entailed by its parents. | Parents are standardised apart; selected pivots become complementary under one valid unifier. | Apply the substitution, check pivot equality and compare every residue literal. |
| The unification output is most general. | Every repair uses a variable absent from its replacement and substitutions are composed. | Verify equality after the MGU and factor any test unifier through it. |
| Resolution is refutation-complete. | The input is a finite first-order clause set and the enumeration of inferences is fair. | Trace Herbrand finite-core, ground-resolution and semi-commutativity steps. |
| Deriving □ certifies unsatisfiability. | Every proof line cites sound parent clauses and a checked resolution step. | Replay the finite proof graph without repeating search. |
| Failure to derive □ is not generally a model certificate. | First-order saturation may continue indefinitely. | Inspect whether genuine finite closure, rather than a resource limit, was reached. |
| Purity and subsumption preserve satisfiability. | Purity is tested against possible key triples; subsumption has an explicit witnessing substitution. | Check the theorem's precondition before each deletion. |
Fidelity, teaching and implementation review
Review one: scholarship. The reconstruction follows the primary's architecture: refutation syntax, Herbrand saturation, ground resolution, the Basic Lemma, substitution composition, disagreement sets, the Unification Theorem, key triples, first-order resolvents, completeness and the final search principles. It preserves the one-way direction of semi-commutativity and does not turn refutation completeness into a universal decision procedure.
Review two: teaching and execution. Ten bespoke SVGs each carry a unique title, description, caption and source scope. Animation reinforces flow but is disabled by reduced-motion preference. Twelve worked examples and twelve causal probes test scope, grounding, occurs-check, variable freshness, MGU generality, closure and safe deletion. The laboratory audits all 1,024 selectable configurations and exposes rather than hides failed unifications.
Terminology review. “Occurs-check”, “factoring” and “semi-decision” are used as modern orientation where helpful; Robinson's own formal roles remain explicit. Most generality is described by factorisation, not by claiming one textual substitution list is uniquely privileged. Purity is not reduced to a naive polarity count when first-order unifiability matters.
Scope review. The paper offers a formal proof calculus and search reductions. It does not claim that the program chooses its own goals, understands a theorem, learns which clauses matter, or possesses consciousness. Machine orientation means that one rule was designed for computational execution and can be checked algorithmically.
Twelve cards for rebuilding the argument
The machine converts relevance from an oracle into a constraint
The proof-set demon names a general problem in intelligent search: a small decisive witness may sit inside an enormous legal space. Unification does not predict relevance from experience. It derives a local relevance condition from the structure of two proposed inference partners. A term is admitted because it repairs a visible disagreement.
Most generality is a discipline of postponed commitment. The MGU performs exactly enough substitution to enable the inference while retaining every degree of freedom that the equality constraints do not settle. This resembles a rational information policy: specialise when forced, preserve options otherwise. The resemblance is structural, not psychological.
Resolution also separates action from control. The inference rule says what child may follow from chosen parents. Purity, subsumption, replacement and scheduling say which state should be retained and which action should happen next. A formal agent can be perfectly sound at the first layer and practically helpless at the second.
The empty clause supplies a crisp goal test, and the proof sequence supplies provenance. Each child remembers a local causal history through parents and unifier. That makes the result auditable even when discovering it exceeded unaided human calculation. The machine's strength is not opacity; it is the repeatability of a larger formal step.
Worked example · commitment delayed by a variable
The clause R(f(y))∨S(y) records a whole family of consequences because y remains free. Only a later pivot that constrains y should specialise it. The variable is not ignorance to eliminate immediately; it exactly represents every still-permitted continuation.
Causal probe · ground every derived clause immediately
Replace each symbolic child with every ground instance up to the current term depth. Soundness remains, but shared structure disappears and the state regains the Cartesian growth resolution was designed to avoid. Representation determines when commitment becomes storage cost.
Boundary statement
Resolution is a calculus for symbolic consequence. It carries no semantics of desire, selfhood or phenomenal experience. Its relevance to agency lies in constrained search, reversible specialisation and verifiable goal completion: not in evidence that proof machinery is conscious.
From ground enumeration to symbolic relevance
Canon 0072 presented Davis and Putnam's quantification procedure: enumerate ground instances, simplify the resulting propositional clauses and search for contradiction. Canon 0073 followed the IBM 704 implementation, where splitting and a tape-backed stack controlled the propositional explosion. Both retained an outer quantifier-free-line generator.
Canon 0074 changes the interface. Robinson's unification folds term selection into first-order inference, while the Resolution Theorem proves that this reordering preserves refutation completeness. The collection moves from global instantiation, through depth-first Boolean control, to a symbolic rule that builds only the common instance needed by a selected pivot.
Canon 0075 turns to Hart, Nilsson and Raphael's formal basis for heuristic minimum-cost path search. The object changes from clauses to paths, but the control question persists: which legal next expansion deserves scarce computation, and what conditions make the chosen order optimal?
What this companion adds
This companion reconstructs Robinson's nineteen-page 1965 paper as one computational argument. It shows why the machine-oriented grain matters, how clauses and the empty clause establish a refutation contract, why Herbrand saturation is both the completeness foundation and a practical burden, how disagreement repair constructs an MGU, and how standardisation apart protects variable scope.
It then follows the exact proof bridge from ground resolution through the Basic Lemma to the Resolution Theorem, distinguishes a finite certificate from a potentially non-terminating search, and treats purity, subsumption and replacement as state-control principles rather than additional laws of inference.
Ten bespoke animated figures, twelve worked examples, twelve causal probes and twelve memory cards make the dependencies inspectable. The executable laboratory implements finite first-order term unification with an occurs-check, constructs resolvents, and audits MGU equality, residue preservation and cyclic-binding rejection across 1,024 selectable configurations.
Primary and comparative sources
- J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle”, Journal of the ACM 12(1), 23–41 (1965). Publisher DOI.
- Martin Davis and Hilary Putnam, “A Computing Procedure for Quantification Theory”, Journal of the ACM 7(3), 201–215 (1960). Publisher DOI.
- Martin Davis, George Logemann and Donald W. Loveland, “A Machine Program for Theorem-Proving”, Communications of the ACM 5(7), 394–397 (1962). Publisher DOI.
- P. C. Gilmore, “A Proof Method for Quantification Theory: Its Justification and Realization”, IBM Journal of Research and Development 4(1), 28–35 (1960). Publisher DOI.
- Jacques Herbrand, Recherches sur la théorie de la démonstration (1930), the finite-ground-instance theorem on which the completeness bridge depends.