A procedure can be complete for proofs without deciding every input
Davis and Putnam begin from a limitation established by Church and Turing, then design inside it. No algorithm can decide validity for every formula of quantification theory. That does not make mechanical theorem-proving empty: valid formulas form an enumerable set, so a well-designed search can eventually expose every valid case.
The paper distinguishes a decision procedure from a proof procedure. A decision procedure halts with the right yes-or-no answer on every admissible formula. Their proof procedure has a narrower contract: when a formula is logically valid, the computation terminates and yields a proof; when it is not valid, the computation may continue without result. The asymmetry is essential, not an engineering defect awaiting a faster computer.
The authors operate by refutation. To prove a formula valid, negate it and seek inconsistency. If the negation cannot be jointly satisfied, the original must be true under every interpretation. That move lets the process focus on increasingly large finite sets of quantifier-free instances. A contradiction appearing in some finite prefix certifies the theorem. Continued consistency of every prefix examined so far does not certify invalidity, because a later instance may create the contradiction.
The historical target was practical as well as foundational. Hao Wang and P. C. Gilmore had produced working proof programs, but the propositional stage became difficult on modest examples. Davis and Putnam looked for a representation in which logical structure could be reduced rather than exhaustively tabulated. Their answer joined an outer Herbrand-style enumerator to an inner clause procedure.
That architecture matters today. A search system should state what kind of non-termination its theory permits, what a positive certificate looks like and which intermediate state can be safely discarded. The paper does all three. It does not confuse “eventually finds every proof” with “quickly answers every question”, nor does it mistake an absence of contradiction at one finite stage for a model of the full first-order formula.
Worked example · prove by refuting
To establish ∀x(P(x)→P(x)), negate it. The negation asserts ∃x(P(x)∧¬P(x)). Replacing the existential witness by a constant a gives the unit clauses P(a) and ¬P(a). Their collision is an explicit finite refutation, so the original universal formula is valid.
Causal probe · demand a negative answer
If the outer procedure were required to halt whenever a formula is invalid, it would become a decision procedure for first-order validity, contradicting the impossibility result that motivates the paper. The non-halting branch is therefore part of the specification.
Syntax is normalised so each later move has a precise object
The procedure does not operate on unrestricted prose-like formulas. It fixes a formal language, moves quantifiers into a prefix and puts the quantifier-free matrix into conjunctive normal form. These transformations create the regular shape needed by the generator and clause rules.
A well-formed formula is assembled from terms, predicate symbols, logical connectives and quantifiers. A sentence has no free variables. An interpretation supplies a non-empty domain, assigns individuals and functions to function symbols, and assigns truth-valued relations to predicates. “Valid” means true under every interpretation; “consistent” means true under at least one. Refutation uses the equivalence between validity of φ and inconsistency of ¬φ.
Prenex form collects quantifiers at the front, leaving a quantifier-free matrix behind. Variable renaming must prevent capture: two quantifiers must not accidentally bind the same textual variable after movement. The authors assume the given formula is prenex when stating the complete algorithm. They also assume the matrix is in conjunctive normal form, a conjunction of clauses, each clause a disjunction of literals.
CNF is not merely cosmetic. It exposes unit clauses, atoms occurring with only one sign and pairs of clauses that can be combined while eliminating an atom. Tautological clauses containing both p and ¬p are always true and may be removed. An empty conjunction represents truth; an empty clause represents falsehood. Confusing those two empty objects reverses the result.
The paper's vocabulary sometimes uses “inconsistent” where contemporary SAT writing says “unsatisfiable”. This companion keeps the historical claim but uses both terms where helpful. The propositional subproblem asks whether a finite conjunction of ground clauses has a truth assignment. The outer first-order problem asks whether the growing set of instances is inconsistent under the Herbrand construction.
Worked example · expose clauses
The formula (p→q)∧(q→r)∧p∧¬r becomes (¬p∨q)∧(¬q∨r)∧p∧¬r. What was a chain of implications is now four clauses. The units p and ¬r make the contradiction mechanically visible.
Causal probe · skip variable renaming
Move quantifiers across connectives while reusing a bound variable name. A formerly independent occurrence may become captured, changing the formula's meaning before the solver begins. No sound clause rule can repair a semantics already altered in preprocessing.
A witness becomes a function of what came before it
The first-order prefix is converted so only universal quantifiers remain. An existential variable is replaced by a fresh function symbol whose arguments are the universal variables preceding that existential. The dependency pattern, not just a new name, is what preserves consistency.
Consider ∀x∃y R(x,y). A single constant for y would claim that one witness works for every x, which is stronger than the original. Instead write R(x,f(x)): the witness may depend on x. In ∀x∀z∃y R(x,z,y), use f(x,z). If an existential quantifier precedes every universal one, its witness has no prior universal dependency and becomes a fresh constant, equivalently a zero-argument function.
The paper presents this replacement in a way that “in essence, goes back to Löwenheim”. Modern texts call it Skolemisation. It preserves satisfiability or consistency, not ordinary logical equivalence sentence by sentence. The expanded language contains new function symbols. A model of the original can interpret them by choosing witnesses; a model of the Skolemised formula immediately supplies witnesses for the existential claims.
Freshness matters. Reusing a function already present could impose accidental equations between unrelated witnesses. Argument order and membership matter too: a Skolem function receives precisely the universally quantified variables in whose scope the existential occurs. Later universal variables cannot influence an earlier existential choice.
After replacement, universal quantifiers can be suppressed for the operational stage. The remaining open matrix is to be instantiated over ground terms built from the newly introduced and already available function symbols. That move does not turn predicates into Boolean variables permanently; each distinct ground atomic formula becomes a propositional atom within a particular finite test.
Worked example · dependency preserved
Transform ∀x∃y∀z∃w R(x,y,z,w). The first witness becomes f(x). The second is allowed to depend on x and z, so it becomes g(x,z). The result is ∀x∀z R(x,f(x),z,g(x,z)). Giving g only x would wrongly forbid w from responding to z.
Causal probe · replace every existential by one constant
For ∀x∃y(y=x), the original is satisfiable in any non-empty domain. Replacing y by one constant a yields ∀x(a=x), false in every domain with more than one object. The intervention destroys consistency preservation by erasing a dependency.
An infinite first-order demand becomes a fair sequence of finite tests
Once existential quantifiers are removed, the procedure builds ground terms and substitutes ordered tuples of them for the remaining universal variables. Each substitution creates a quantifier-free line. Fair ordering ensures that every required finite instance eventually appears.
Ground terms contain no variables. Begin with constants; if the transformed language has none, introduce one. Apply function symbols to already available ground terms, then apply them again to the results. With constant a and unary function f, the sequence includes a, f(a), f(f(a)) and so on. With multiple symbols and arities, the term universe branches rapidly.
For L universal variables, enumerate L-tuples of ground terms in lexicographic order as the paper specifies, then substitute the nth tuple into the quantifier-free matrix to obtain line n. The conjunction of the first n lines is an ordinary propositional formula once each ground atom is treated as a propositional variable. The inner procedure tests that finite conjunction for consistency.
The logical bridge is compactness in operational form: the infinite set of ground instances is inconsistent if and only if some finite subset is inconsistent. Fair enumeration means a finite contradictory subset will eventually be contained in a tested prefix. Hence a valid original formula eventually produces a refutation. If every finite prefix tested so far is consistent, nothing yet licenses termination.
Testing need not occur after every new line. Davis and Putnam discuss intermittent testing because propositional analysis itself has a cost. Larger batches reduce how often the solver is restarted, but may overshoot the first contradictory prefix. Smaller batches detect early contradictions sooner but repeat more work. That is a scheduling policy layered over the completeness requirement that the tested prefixes keep growing without bound.
Worked example · term tuples
With constant a, unary f and two universal variables x,z, early tuples may be (a,a), (a,f(a)), (f(a),a), (f(a),f(a)), then tuples containing f(f(a)). Substituting each pair into R(x,f(x),z) produces a concrete line whose atoms can enter a finite clause set.
Causal probe · unfair enumeration
Suppose the generator endlessly varies only the first coordinate and never assigns f(a) to the second. A contradiction requiring z=f(a) is never exposed. Each tested prefix may be handled perfectly, yet the outer proof procedure loses completeness.
Conjunctive normal form turns truth into a manipulable database
The inner problem is a finite set of clauses. A clause is satisfied when at least one literal is true; the whole formula is satisfied only when every clause is. This representation lets the procedure remove information that no longer affects consistency and combine information that does.
Treat conjunction as a set of obligations and disjunction as alternatives inside each obligation. The clause (p∨¬q∨r) says at least one of those three literals must hold. Repeated literals add nothing. A clause containing p and ¬p is a tautology and constrains no assignment, so it can be deleted. Duplicate clauses likewise need appear only once.
The empty clause has no satisfying literal and is therefore false. Its appearance proves inconsistency. By contrast, if all clauses are deleted, no obligations remain and the empty conjunction is true. This identity convention drives the terminal cases of every SAT implementation derived from the paper.
CNF also localises the effect of assigning an atom. Setting p=true deletes every clause containing p because it is satisfied, and removes ¬p from the remaining clauses because that alternative is false. Setting p=false does the symmetric operation. A unit clause fixes which of these two substitutions can possibly satisfy the conjunction.
The paper compares CNF with truth tables, disjunctive normal form and Gentzen-style branching. It does not claim that CNF prevents exponential size in all circumstances. Indeed, eliminating an atom can generate the Cartesian product of its positive and negative clause families. The structural advantage is that reductions often collapse a practical instance before the worst case is reached.
Worked example · two meanings of empty
From p and (¬p∨q), unit propagation sets p=true, deletes the first clause and shrinks the second to q. Setting q=true then deletes the last clause: satisfiable. If ¬q were also present, propagation would eventually create an empty clause: unsatisfiable.
Causal probe · treat an empty clause as success
A solver that sees [] and reports “no literals left, so nothing remains” confuses a false disjunction with a true conjunction. The formula p∧¬p would then be misclassified as satisfiable. Typed representations should distinguish a clause from a clause set.
A one-literal clause forces an assignment through the whole formula
If a clause contains only p, any satisfying assignment must make p true. If it contains only ¬p, p must be false. Davis and Putnam use that necessity to simplify every occurrence, repeating until no unit clause remains or contradiction is exposed.
With unit p, delete clauses containing p: they are already satisfied. From every remaining clause, delete ¬p: that literal can no longer satisfy anything. The transformation preserves consistency because it is exactly substitution of the only permitted value. A unit ¬p performs the inverse substitution.
If both p and ¬p appear as unit clauses, no assignment can satisfy both. More generally, propagation may shorten another clause to emptiness. That empty clause is the paper's route to declaring the finite conjunction inconsistent. In the complete algorithm, inconsistency can be concluded only through this rule, after other transformations have created or exposed the conflict.
Unit propagation is recursive. One forced value can shorten a binary clause into a new unit, which forces another value, and so on. The resulting cascade is a deductive chain inside a consistency test. Its order does not change satisfiability, although it changes the trace and may affect performance.
The 1962 Davis–Logemann–Loveland program retained this rule but changed how hard cases were treated, using case splitting instead of eliminating a variable by all resolvents. Modern SAT solvers elevate propagation into an intensely optimised kernel. That later lineage should not obscure the 1960 rule's exact role: it is a semantics-preserving simplifier within both the paper's examples and complete loop.
Worked example · implication chain
Start with p, (¬p∨q), (¬q∨r), ¬r. Unit p produces q; q produces r; r conflicts with ¬r. Four clauses that admit no assignment collapse to the empty clause without enumerating eight truth assignments.
Causal probe · delete the wrong polarity
After unit p, remove p from every clause instead of deleting clauses that contain it. The satisfied clause (p∨q) would become q, inventing a requirement that q be true. The correct operation distinguishes “this clause is satisfied” from “this literal is false”.
An atom with only one polarity can be satisfied and forgotten
If p occurs affirmatively but never as ¬p, set p=true and delete every clause containing it. If it occurs only negatively, set p=false. No remaining clause can object, so consistency is preserved.
This affirmative-negative rule is now called pure-literal elimination. Its logic differs from unit propagation. A unit literal is forced in every satisfying assignment. A pure literal need not take its satisfying value in every model; rather, if any model exists, changing that atom to satisfy all of its occurrences cannot damage another clause because the opposite sign is absent.
Suppose F=(p∨q)∧(p∨¬r)∧(q∨r). Atom p is pure positive. Setting p=true deletes the first two clauses, leaving q∨r. The reduced formula is satisfiable exactly when the original is. The rule can reveal new pure literals or units, so the complete procedure cycles back rather than applying each rule once.
Purity is relative to the current clause set. An atom that appeared with both signs can become pure after satisfied clauses are removed. Conversely, deciding purity from the original input and caching it forever is unsafe because transformations change which clauses remain. The property must be recomputed or maintained correctly.
The rule is particularly valuable because it removes clauses without producing new ones. Yet it does not by itself prove that a non-empty formula is inconsistent. If every clause disappears, consistency is established for the finite conjunction. If impure atoms remain, elimination or further propagation is required.
Worked example · purity without necessity
In (p∨q)∧(p∨¬q), p is pure and the formula is satisfiable by p=true. But p is not logically forced: q=true, p=false fails the second clause, whereas q=false, p=false fails the first, so here p happens to be forced; add a third variable as (p∨q)∧(p∨r) and p=false remains possible when q=r=true. Purity still permits choosing p=true without loss.
Causal probe · misread absence as falsity
If ¬p is absent, setting p=false rather than true can shrink all p-clauses and manufacture a conflict. The rule works because it chooses the polarity that satisfies every occurrence, not because missing negative evidence counts as evidence for falsehood.
Resolve opposite occurrences, then eliminate the atom
When p appears with both signs and no simpler rule applies, collect clauses containing p and clauses containing ¬p. Combine their remaining parts pairwise. The resulting resolvents express exactly the compatibility conditions needed after p is forgotten.
Take (p∨A) and (¬p∨B), where A and B stand for disjunctions not containing p. At least one clause will be threatened whichever value p receives. Their resolvent A∨B must therefore hold. Rule III forms all such cross-pairs, retains clauses not mentioning p and removes the parent clauses. Tautological resolvents can be discarded.
For the whole formula, write P for the conjunction of p-clauses, N for the conjunction of ¬p-clauses and R for clauses free of p. Eliminating p produces R together with every resolvent between P and N. The paper justifies that the original and result are equiconsistent. In modern terms, the transformation existentially projects p out of a CNF relation.
Resolution can shrink variable count while expanding clause count. If p occurs in m positive and n negative clauses, as many as mn resolvents may be generated before tautology and subsumption removal. That is the central worst-case hazard. The paper's statement that the propositional cycle needs at most 2(R−1) rule steps counts eliminations and intervening reductions; it does not bound the size of the formulas created at those steps.
This is the operation historically associated with the Davis–Putnam procedure. It is not the same as the later DPLL split that recursively tries p=true and p=false. Nor is it identical to Robinson's 1965 first-order resolution with unification. All belong to a resolution lineage, but their states and completeness arguments differ.
Worked example · eliminate p
From (p∨q), (p∨r) and (¬p∨s), eliminating p yields (q∨s) and (r∨s). Any assignment to q,r,s satisfying these resolvents can be extended with a suitable p; any model of the original satisfies both resolvents.
Causal probe · keep only one resolvent
Drop (r∨s) from that example. Let q=true, r=false, s=false. The surviving resolvent is satisfied, but no p can satisfy both (p∨r) and (¬p∨s). Omitting a cross-pair breaks equiconsistency.
Generate, reduce, eliminate, then either refute or enlarge
The paper's complete algorithm interlocks two loops. Step 1 enlarges the first-order instance set. Steps 2–4 decide the consistency of that finite propositional conjunction. A consistent finite answer sends control back outwards; an inconsistent answer ends the entire refutation.
Step 1 generates one more quantifier-free line and forms the conjunction of all lines produced so far. Step 2 repeatedly applies the one-literal rule. If an empty clause is reached, the conjunction is inconsistent. If every clause disappears, it is consistent. Otherwise control moves to Step 3.
Step 3 repeatedly removes atoms occurring only affirmatively or only negatively, returning to Step 2 whenever units appear. If all clauses disappear, the current finite conjunction is consistent. If every remaining atom occurs with both signs and no units remain, control moves to Step 4.
Step 4 selects the first atom from a shortest clause under the paper's specified ordering, eliminates it using Rule III, restores CNF and returns to Step 2. The heuristic is part of the procedure as written, but equiconsistency does not depend on that particular variable order. Different choices can change intermediate size enormously.
If the finite conjunction is consistent, generate more ground lines. If it is inconsistent, the negated target has no model and refutation is complete. Thus each finite SAT episode terminates because rules remove clauses, assign atoms or eliminate an atom; the outer sequence may continue indefinitely. Two levels of termination must never be collapsed into one marketing claim.
Worked example · one full pass
For clauses p, (¬p∨q), (¬q∨r), (s∨r), (¬s∨r), ¬r, Step 2 propagates p, q and r. The unit ¬r then collides, so the finite conjunction is inconsistent before pure-literal deletion or general elimination is needed.
Causal probe · stop after a consistent prefix
Let the first ten ground lines be jointly consistent and line eleven introduce an instance contradicting them. Returning “invalid” after ten lines mistakes provisional survival for a first-order countermodel. The algorithm explicitly goes back to Step 1.
Fewer rule steps do not guarantee a small intermediate formula
Davis and Putnam report that their propositional method terminates in at most 2(R−1) steps for R variables, contrasting that linear step count with truth-table branching. They immediately warn that the formulas produced can be much more complicated than the input.
A step count is meaningful only alongside the size of a step. Eliminating p from m positive and n negative clauses may form mn resolvents. Repeating elimination can fill in a clause graph much as eliminating variables in graphical models creates larger factors. A short sequence of enormous transformations can be harder than many cheap assignments.
The selection heuristic: take the first atom in a shortest clause: tries to exploit constrained variables. It is not presented as an optimality theorem. Modern elimination heuristics estimate resolvent growth, remove subsumed clauses and detect tautologies aggressively. These refinements retain the same semantic invariant while changing the operational profile.
The authors compare their hand calculation with Gilmore's IBM 704 run on one formula. Gilmore's routine ran for 21 minutes without a result after effectively generating seven quantifier-free lines. Their intermittent test examined prefixes at 10, 20 and 30 lines, with the first inconsistent prefix later found at 21, and the hand computation took about 30 minutes. This is an illuminating case study, not a statistically controlled benchmark.
The evidence supports the claim that propositional processing, rather than instance generation alone, was a crucial bottleneck in that example. It does not establish a universal speed ratio, hardware-independent superiority or absence of exponential behaviour. The paper itself is candid about formula growth and says the method does not “ordinarily” lead to exponentiation, a practical observation rather than a worst-case bound.
Worked example · clause multiplication
If p occurs positively in 12 clauses and negatively in 15, naive elimination considers 180 parent pairs. Many resolvents may be tautological or duplicated, but none can be assumed away before inspection. One variable has vanished while the database may have grown.
Causal probe · report only eliminations
Benchmark two solvers by the number of eliminated atoms and ignore clauses generated. The solver producing a million resolvents appears equal to one producing ten. The metric hides the work responsible for memory and runtime.
Twenty-one lines expose what seven lines cannot
The final section works a formula previously used by Gilmore. Its pedagogical force lies in the trace: the same logical target looks intractable under one propositional treatment and manageable when clauses are repeatedly reduced.
The authors negate the target, put its matrix into CNF and replace an existential variable by a function term. They generate ground instances and adopt intermittent testing at prefixes of ten, twenty and thirty lines. The conjunction remains consistent at ten and twenty, but is inconsistent at thirty; later inspection finds twenty-one is the smallest inconsistent prefix.
That minimum matters. Gilmore's run had produced the equivalent of seven lines, so it had not yet accumulated enough instances for any sound propositional procedure to refute the formula. Yet the authors argue that its disjunctive-normal-form processing was already consuming the machine. Their method could manipulate a larger evidential prefix by avoiding the same form of expansion.
The worked calculation applies unit deletion and variable elimination to a dense symbolic clause list. It is not presented as a polished machine trace: the claimed improvement was demonstrated by hand, and the authors explicitly say a machine program had not yet been constructed. The next canon paper, by Davis, Logemann and Loveland, is the implementation report and algorithmic modification.
Reading the example fairly requires preserving that boundary. The 1960 paper offers a complete logical procedure, local complexity observations and one comparative calculation. It does not yet report a production solver, a benchmark suite or automatic proof certificates in a modern exchange format. Its contribution is the transform architecture that made such engineering plausible.
Worked example · schedule trade-off
Testing at n=10,20,30 finds inconsistency on the third test, even though n=21 is sufficient. Testing every line would locate 21 exactly but run the finite solver twenty-one times. The best schedule depends on solver restart cost and expected contradiction depth.
Causal probe · generalise from one comparison
Change the formula family so variable elimination produces huge resolvent sets while truth-table pruning succeeds early. The reported advantage may reverse. A case study diagnoses a bottleneck; it does not rank all proof procedures on all inputs.
DP, DPLL and first-order resolution are related but not interchangeable
Later terminology often compresses several developments into “the Davis–Putnam algorithm”. Precision matters because each procedure changes a different object and pays a different cost.
The 1960 propositional core eliminates a variable by generating all required resolvents between its positive and negative occurrences. The complete first-order procedure surrounds that core with Skolemisation and Herbrand-style ground-line generation. It is a proof procedure for quantification theory, not merely a SAT solver presented in isolation.
The 1962 Davis–Logemann–Loveland program modifies the propositional strategy. It retains unit reasoning and uses a splitting rule: choose an atom, try one truth value and backtrack to the other if needed. That avoids eagerly materialising every resolvent for the chosen variable. Modern DPLL names the later branching family; using DPLL as a label for every step of the 1960 paper obscures the change.
Robinson's 1965 resolution principle works directly with first-order clauses by unifying terms, combining substitution and truth-functional inference. Davis–Putnam resolution is already present at the propositional level, but it operates after ground instances have been generated. Robinson's unification-based system attacks the alternation between substitution and propositional analysis that the earlier architecture kept as two interlocking parts.
Cook's 1971 result later identifies propositional satisfiability as a central complexity problem by establishing polynomial reductions from nondeterministic polynomial-time recognition. That does not retroactively make Davis and Putnam's heuristic claims complexity-theoretic results. It explains why no collection of clever local reductions should be expected to remove worst-case difficulty without a profound consequence.
Worked example · elimination versus split
With twenty positive and twenty negative p-clauses, DP may build four hundred resolvents. DPLL instead explores p=true and, if necessary, p=false, simplifying clauses in each branch. One may repeat work across branches; the other may spend memory up front. Their shared literals do not imply identical execution.
Causal probe · add first-order variables to propositional resolution
Resolve P(f(a))∨Q with ¬P(x)∨R without finding a substitution for x. Treating the atoms as unequal misses the inference; treating them as equal without justification is unsound. Robinson's unification supplies the missing mechanism.
Watch three rules preserve satisfiability
Five controls build a clause set over p, q, r and s. The laboratory applies unit propagation, pure-literal elimination and Davis–Putnam variable elimination, while an independent truth-table oracle checks the answer. The audit covers all 4⁵=1,024 control combinations.
Running exact audit…
Running transformation audit…
Running terminal-state audit…
Worked example · change a unit
Keep the four binary clauses fixed and switch Clause 5 from p to ¬p. The reduction trace shows which clauses disappear and which literals become forced. Changing one factual commitment can redirect the entire proof without changing the rules.
Causal probe · choose a harder polarity pattern
Select signs so every variable appears both positively and negatively after the initial unit cascade. Pure-literal deletion stops helping, and the trace must use cross-resolvents. This intervention isolates why Rule III is necessary.
What was checked, and under which condition
| Claim | Condition | Audit handle |
|---|---|---|
| Replacing existentials by fresh functions preserves consistency. | Each function depends on exactly the preceding universal variables; symbols are fresh. | Construct models in both directions and test dependency-changing counterexamples. |
| Fair ground-line generation eventually exposes every finite refutation. | Every ground tuple occurs and tested prefixes grow without bound. | Track tuple coverage; inject a contradiction requiring a deliberately delayed term. |
| Unit and pure-literal reduction preserve satisfiability. | Clause satisfaction and false-literal deletion use opposite actions. | Compare each transformed set with all truth assignments over the remaining variables. |
| Rule III eliminates an atom without changing consistency. | Every positive–negative pair contributes a resolvent; only tautologies and duplicates are discarded. | Brute-force parent and result sets for small vocabularies. |
| The inner propositional procedure terminates. | Each cycle assigns, removes or eliminates an atom and finite clauses are maintained. | Require a decreasing variable measure and explicit empty states. |
| The complete first-order procedure halts on valid formulas. | Preprocessing is sound, enumeration is fair and the finite solver is complete. | Verify a finite contradictory prefix exists and is eventually included. |
| The reported comparison shows a useful practical case. | It concerns one formula, a hand computation and a historical machine run. | Preserve n=7, test points 10/20/30, minimum inconsistent prefix 21 and the reported times. |
Fidelity, teaching and implementation review
Review one: scholarship. The companion follows the paper's six-section order and keeps its central distinctions intact: validity versus consistency, decision versus proof procedure, finite propositional termination versus possible infinite first-order search, and consistency preservation versus formula equivalence. The three rules match the primary. The empirical comparison is reported with its stated limits. Later terms: Skolemisation, SAT, DPLL, unification and NP-completeness: are marked as later context rather than inserted into the 1960 authors' vocabulary.
Review two: teaching and execution. Each abstraction is paired with a worked example and an intervention that would break it. Ten SVG figures carry unique titles and descriptions, motion honours reduced-motion preference, colours are not the sole signal and mobile tables scroll. The laboratory has an independent truth-table oracle, exhaustively covers 1,024 selectable formulas and checks transformation and terminal invariants. The prose avoids fabricated quotation, anthropomorphic claims and inflated relevance to consciousness.
Evidence fairness. The article does not turn “does not ordinarily lead to exponentiation” into a worst-case guarantee. It distinguishes the 30-minute hand calculation from a machine implementation and does not infer general superiority from one example. It names the Air Force support noted in the primary without making sponsorship a substitute for analysing the mathematics.
Boundaries. This is a symbolic procedure over a declared formal language. It does not learn predicates from data, revise goals, perceive a world or establish consciousness. Its relevance to agency is architectural: transform a goal into checkable obligations, maintain semantics under compression and recognise a conclusive certificate.
Twelve cards for rebuilding the procedure
The durable idea is semantics-preserving state reduction
The paper can be read as a design manual for exact symbolic search. First expose a certificate condition: inconsistency. Then normalise the problem so every state has a regular representation. Separate unbounded evidence generation from a bounded decision kernel. Within the kernel, apply transformations only when their preserved property is stated and proved.
Each clause rule is a different kind of compression. Unit propagation conditions on a necessary value. Pure-literal elimination chooses a harmless value that can satisfy all one-sided occurrences. Resolution projects out a variable while retaining every compatibility constraint. Their operational shapes differ because their proofs differ.
This vocabulary carries into planning, constraint solving and verification. A system may discard alternatives when it retains a sufficient summary for the property being decided. But the analogy stops where the invariant stops. Deleting a dominated plan, marginalising a probabilistic variable and resolving a Boolean atom are not automatically equivalent just because all reduce state.
Agency enters only in a modest formal sense. The machine pursues a fixed certification goal through rule-governed transformations. It has no account of how the goal was chosen or whether its predicates correspond to a changing environment. What it demonstrates is how apparent search can become reliable action when every irreversible transformation comes with a semantic contract.
Boundary statement
No result in the primary establishes intelligence or consciousness. The work contributes a proof architecture: formal input, explicit target, fair expansion, semantics-preserving reductions and a terminal certificate. Claims beyond that require independent theory and evidence.
From weighted frontiers to logical search
Canon 0071 made a locally smallest graph choice permanent under a cut or distance invariant. Canon 0072 replaces numerical order with logical consequence. A clause is shortened, removed or combined only when consistency is preserved. Both papers show that global correctness depends less on the surface form of a local move than on the state invariant surrounding it.
Canon 0073 follows the procedure into an actual IBM 704 program. Davis, Logemann and Loveland revise the propositional strategy, making explicit the split-and-backtrack mechanism now associated with DPLL. The transition is ideal for the canon: a mathematical procedure encounters memory and runtime, then changes shape under implementation pressure.
What this companion adds
This companion reconstructs all six substantive parts of Davis and Putnam's 1960 paper: the proof-procedure contract, formal language, witness functions, ordered quantifier-free lines, normal-form comparison, three propositional rules, complete interlocking algorithm and historical example. Modern vocabulary is used as a bridge and dated explicitly.
Ten bespoke animated figures, twelve memory cards, twelve worked examples and twelve causal probes make every invariant inspectable. The executable laboratory explores 1,024 clause sets, compares the Davis–Putnam verdict with a truth-table oracle and audits every local transformation for equisatisfiability.
The source record is anchored in the fifteen-page Journal of the ACM scan and DOI metadata. Later comparisons are limited to primary papers by Davis, Logemann and Loveland, Robinson and Cook, plus the contemporaneous Gilmore and Wang sources named by Davis and Putnam.
Primary and comparative sources
- Martin Davis and Hilary Putnam, “A Computing Procedure for Quantification Theory”, Journal of the ACM 7(3), 201–215 (1960). Publisher DOI; archival scan.
- 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; archival scan.
- J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution Principle”, Journal of the ACM 12(1), 23–41 (1965). Publisher DOI.
- Stephen A. Cook, “The Complexity of Theorem-Proving Procedures”, Proceedings of the Third Annual ACM Symposium on Theory of Computing, 151–158 (1971). 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.
- Hao Wang, “Toward Mechanical Mathematics”, IBM Journal of Research and Development 4(1), 2–22 (1960). Publisher DOI.