Martin Davis and the Logic of a Checkable Plan

A student takes a question home

As an undergraduate at City College, Davis read a remark by his teacher Emil Post about the tenth problem on David Hilbert’s list. Given a polynomial equation with integer coefficients, could anyone devise a procedure that would always decide whether the equation had a solution in integers? Post suspected that the search for such a procedure would end in a proof of impossibility. Davis later recalled how the question kept drawing him away from the subject he had chosen for his doctoral research. Born in New York in 1928, he graduated from City College in 1948 and completed his doctorate under Alonzo Church at Princeton in 1950. Davis’s recollections · Princeton’s biographical record.

That summer he met Julia Robinson at the International Congress of Mathematicians in Cambridge, Massachusetts. They had come at Hilbert’s problem from different directions. Seven summers later, Davis and Hilary Putnam shared a house with their families during a logic institute at Cornell. They talked mathematics, but also found time to trade lessons in philosophy and functional analysis. A joint line of work by Davis, Putnam and Robinson eventually brought the problem within reach. In 1970 Yuri Matiyasevich supplied the decisive missing step. Particular equations could still be solved. What the four mathematicians’ work ruled out was a single algorithm guaranteed to answer correctly for every equation of this kind. Davis on the collaboration · Robinson’s account.

The alternative on the tape

Another part of Davis’s working life was spent close to the machinery. At the University of Illinois he helped program the early computer ORDVAC. In 1960 he and Putnam published a procedure for theorem proving. It repeatedly called for a more restricted question to be answered. Given a finite list of statements joined by “and”, with alternatives linked by “or” inside each statement, was there any assignment of true and false that would satisfy the whole list? This is the Boolean satisfiability problem, usually called SAT. Princeton on the Illinois years · The 1960 paper by Davis and Putnam.

In the first implementation, eliminating a proposition could leave a great many longer statements in its place. Fast memory on the IBM 704 was scarce. In 1962 Davis, George Logemann and Donald Loveland described a different choice. If the rules already forced a value, the machine used it. When a choice remained, it could try one value and keep the alternative on tape. The most recently saved alternative was the first one recovered. The authors reported frankly that the theorems they had managed to prove were more modest than they had hoped. The procedure for the finite Boolean part endured. Its familiar initials, DPLL, preserve the names of all four contributors across the two papers. The 1962 paper, pp. 394–395 · Courant’s account of Davis’s work.

When a solution describes a plan

Thirty years later, Henry Kautz and Bart Selman proposed expressing a planning problem in this same language. Write down the starting situation, the actions available, what each action requires and changes, and what must hold at the end. Give the plan a fixed number of steps. A satisfying assignment can then tell you which actions to take. In a later assessment Kautz recalled how far the idea had seemed from a practical planner in 1992. By 2004, Satplan had taken first place in optimal STRIPS planning at an international planning competition. Kautz and Selman’s original proposal · Kautz on the development of Satplan.

Consider a robot asked to deliver a part. At the step where it picks the part up, the robot and the part must be in the same place. At the step where it puts the part down, it must still be carrying it. A reader can follow a proposed plan from the initial state and check both conditions. If the rules admit no plan in the allotted steps, a longer plan may still exist. And if going through a doorway requires a permit, the plan can establish compliance only if that requirement made it into the rules.

What a second reader can check

Repeating a search and verifying its answer are different tasks. A fixed order for exploring the alternatives can make a search repeatable. Anyone given a satisfying assignment can check each clause without repeating that search. A claim that every possible assignment fails calls for different evidence. Later researchers developed ways for a solver to supply a proof of contradiction that another program could check. Luis Cruz-Filipe and colleagues demonstrated this with two certified checkers for the LRAT proof format, one in Coq and the other in ACL2. Here the reader can ask for the evidence behind a negative answer, even when the search that found it was long. The paper on certified proof checking.

Davis helped found the computer science department at New York University and remained at its Courant Institute until his retirement in 1996. He died on 1 January 2023. Robinson left a more personal record of their collaboration. On 15 February 1970, it was Davis who telephoned her from New York with the news of Matiyasevich’s breakthrough. For years, she recalled, she had made the same wish when she blew out her birthday candles. She wanted to live long enough to know the answer. New York University · Robinson remembers the telephone call.

A chronology

1. 1928–1950 · New York and PrincetonBorn in New York. Earns his mathematics degree in 1948 and his doctorate in 1950.
2. 1960 · Automated reasoningPublishes a theorem-proving procedure with Hilary Putnam.
3. 1962 · Reasoning by casesDescribes the IBM 704 program with George Logemann and Donald Loveland.
4. 1965–1996 · New York UniversityServes on the Courant faculty and helps establish the computer science department.
5. 1970 · Hilbert’s tenth problemMatiyasevich completes the argument built on work by Davis, Putnam and Robinson.
6. 2023Dies on 1 January.