Pith. sign in

REVIEW 2 major objections 4 minor 97 references

Martin Davis: An Overview of his Work in Logic, Computer Science, and Philosophy

T0 review · 2 major / 4 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read The paper argues that logic, not computer science, was the unifying theme of Martin Davis's career, tracing his work from unsolvability and the DPRM theorem to automated reasoning and the philosophy of computing.

desk verdict A useful, mostly reliable survey of Martin Davis's work; the Section 3 'cannot overestimate' line is rhetorical overreach, but the underlying case for Davis's centrality is solid. read the letter →

arxiv 2506.08588 v1 pith:SC5MJY7Q submitted 2025-06-10 cs.LO

Liesbeth De Mol , Yuri V. Matiyasevich , Eugenio G. Omodeo , Alberto Policriti , Wilfried Sieg , Elaine J. Weyuker This is my paper
classification cs.LO MSC 01A7003D2503D3511U05
keywords MartinDavisbiographycomputabilitytheoryHilbert'sTenthProblemDPRMtheoremautomatedreasoningDPLLChurch-Turingthesishistoryofcomputing
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Martin Davis spent more than seventy years moving between mathematical logic, computer science, and philosophy, and this paper argues that logic was the thread that held the whole career together. The authors reconstruct Davis's path from his 1950 doctoral thesis, which recast recursive function theory through Emil Post's normal systems, through his conjecture that every listable set of natural numbers is Diophantine, proved with Julia Robinson and Yuri Matiyasevich as the DPRM theorem, and through the Davis-Putnam and DPLL procedures that still sit at the core of modern SAT solvers. On the historical and philosophical side, they present Davis as a mechanist who defended the Turing-Post analysis of computability against hypercomputation and Penrose's Gödel-based arguments. The payoff of the paper's thesis is a unified portrait: the same logical viewpoint that made Davis a founder of theoretical computer science also shaped his historical writings, his nonstandard analysis textbook, and his philosophy of mathematical practice.

What carries the argument

The argument's main mechanism is a thematic tour of Davis's own writings, tied together by his repeatedly stated self-conception as a logician. The technical anchors are Davis's normal form, the 1953 theorem that every listable set can be represented by a polynomial equation whose only universal quantifier is bounded, and his bold conjecture that every listable set is Diophantine. The DPRM theorem, which completed the conjecture, shows that the concept of computability can be defined in purely number-theoretic terms. On the computational side, the DP and DPLL satisfiability procedures and the Linked Conjunct method serve as evidence that Davis's logic-first approach produced working tools for automated deduction; on the philosophical side, Davis's mechanist and anti-dogmatic empiricist stance, spelled out in 'Pragmatic Platonism', ties the technical work to a wider worldview.

What would settle it

An archival study comparing Davis's recollections with the actual drafts, referee reports, and letters around the DPRM theorem and the 1960s SAT work could settle the account. If it showed, for example, that Putnam or Robinson independently arrived at key reductions without Davis, or that the original DP report's SAT focus came entirely from NSA direction rather than Davis's agenda, the paper's central portrait of Davis as the logic-driven protagonist would be falsified.

Watch

Extended reading notes

Core claim

The paper's central claim is that Martin Davis's scientific identity was, as he himself said, that of a logician. It treats the title change from 'From logic to computer science and back' (1999) to 'My life as a logician' (2016) as the key to interpreting his oeuvre. The authors argue that this single identity explains the coherence of his landmark contributions: in computability theory, his dissertation and textbook recast the subject around Turing machines and Post's production systems and gave it the name 'computability theory'; in number theory, his normal form theorem and his conjecture that every listable set is Diophantine supplied the framework that ended with the DPRM theorem and the negative solution of Hilbert's Tenth Problem; in automated reasoning, his work with Putnam, and then Logemann and Loveland, produced the DP and DPLL procedures that remain the backbone of SAT solving; and in history and philosophy, Davis used the same logical standpoint to defend the Church-Turing analysis against hypercomputation and to write the history from Leibniz to Turing as the prehistory of the computer.

Load-bearing premise

The load-bearing premise is that Davis's own self-description and the authors' insider recollections are historically reliable; if those memories and letters systematically exaggerate Davis's role, the claimed unified vision of his career would collapse into a retrospective narrative.

Editorial extensions

If this is right

  • If the paper's portrait is right, Davis's 1958 textbook Computability and Unsolvability should count as one of the founding texts of theoretical computer science, since it deliberately rebranded recursive function theory as computability theory.
  • The DPRM theorem means Hilbert's Tenth Problem is undecidable and that effective computability can be captured by polynomial equations alone, so the notion of algorithm has a purely mathematical characterization.
  • Because DPLL remains the core engine of modern SAT solvers, Davis's 1960s work with Putnam, Logemann, and Loveland has direct descendants in today's verification and automated-reasoning tools.
  • The historical essays argue for a diversified history: the Church-Turing thesis is not one thesis, and Post's anticipation deserves recognition alongside Turing's analysis of computation.
  • Davis's criticisms of hypercomputation imply that proposed models that compute beyond Turing machines only work by dropping finiteness conditions essential to Turing's analysis of computability.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial extension: a testable reading of this overview is that Davis's textbooks and technical papers should be studied as philosophical documents, not just as mathematics; archivists could check Davis's unpublished correspondence with Post, Robinson, and Putnam to see whether the 'logic first' self-image shaped the historical record or reflected it.
  • If the paper's emphasis on Post is right, then standard histories of theoretical computer science might be reweighted: Post's normal systems and production rules deserve credit as a direct ancestor of both computability theory and modern SAT and rewriting ideas, a shift the paper suggests but does not fully develop.
  • The paper notes the early hope that Diophantine machines could bear on P versus NP but does not pursue it; a natural extension would be to ask whether the DPRM theorem's parameterized polynomial representations can be used to separate complexity classes, though nothing in the paper guarantees such a route works.
  • Davis's 'Pragmatic Platonism', the view that knowledge of abstract mathematical worlds is reliable but fallible, could be imported into current debates about AI and mathematical proof, since it offers a philosophical stance on computer-generated mathematics that the paper only sketches.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 4 minor

Summary. The paper surveys Martin Davis's contributions to computability theory, Hilbert's Tenth Problem, automated reasoning, nonstandard analysis, and the history and philosophy of computing, and argues that logic was the unifying thread of his career. The mathematical content is presented accurately, with careful accounts of the Davis normal form, the DPRM theorem, and the DPLL procedure, and the historical narrative is densely referenced, drawing heavily on Davis's own recollections and the memoirs of collaborators. The central claim is that a consistent vision, centered on logic, illuminates Davis's body of work from his 1950 dissertation through his later historical and philosophical writings.

Significance. If its historical thesis is accepted, the paper provides a valuable unified perspective on Davis's career and supplies a useful entry point to the primary literature. Its technical exposition is reliable: the statements of the Davis normal form, the DPRM theorem, and the DPLL algorithm are correct, and the paper credits the full chain of contributors to the DPRM result. The authors' insider knowledge yields concrete details and personal recollections that are not available in more detached accounts. However, the insider perspective also creates a methodological risk, since several authors were participants in the events described and much of the evidence comes from retrospective self-reports.

major comments (2)
  1. [Section 3] The sentence 'One cannot overestimate the role played by Davis in resolving Hilbert's Tenth Problem' is an unqualified superlative that is not supported by the evidence presented. The surrounding narrative relies on Davis's own Foreword [31], his recollections [39, 41], and the account of Matiyasevich, who is a coauthor of this paper. No independent archival sources (e.g., the Davis-Putnam-Robinson correspondence or contemporaneous letters) are cited to corroborate the attribution of indispensability. This makes the claim an assertion of historical priority rather than a demonstrated result. The authors should either soften the sentence to a more measured claim, such as 'Davis played a central role,' or add independent documentary evidence that verifies the sequence of contributions.
  2. [Section 6] The concluding sentence 'For us it is clear that Davis became through his work an integral part of "their story"' is presented as a self-evident conclusion, but it rests on the same retrospective sources that the paper uses throughout: Davis's own autobiographical essays, his recollections of collaborations, and the recollections of coauthors, including the authors themselves. Given that the paper's aim is to provide a 'consistent vision,' the authors should explicitly address the methodological implications of their dual role as participants and historians. A short paragraph acknowledging the potential for selection bias in the choice of episodes and interpretations, and explaining why the narrative remains reliable, would substantially strengthen the paper's historical credibility.
minor comments (4)
  1. [Section 3, footnote 7] The phrase 'Presumably, this was Raphael Robinson' is speculation without a cited basis; it would be appropriate to write 'possibly Raphael Robinson' or to find documentary evidence before asserting a likely identification.
  2. [Section 2] The claim that Davis's 1958 textbook 'Computability and Unsolvability' was 'one of the founding texts of an emerging new field, computer science' is plausible but would benefit from a supporting citation showing its reception or influence, such as later citations or adoption in courses.
  3. [Section 6] The sentence 'Davis's work here was heavily influenced by his own experience as a logician who became involved with programming early on' is an interpretive claim about causation; the paper does not offer evidence that this experience shaped his historical writings in particular, as opposed to his technical work.
  4. [Section 3] The remark that Matiyasevich called Davis's conjecture 'bold' would benefit from a specific citation to the work in which this characterization appears, as the current text does not give a reference for that quotation.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is a historical survey with no derivation chain, and insider recollections function as primary-source testimony rather than a circular reduction.

full rationale

This paper is a historical and expository survey, not a derivation: it reports Davis's theorems (normal forms, DP/DPLL, nonstandard analysis, DPRM) from the published literature and does not fit parameters or derive predictions from inputs. The closest self-referential element is that the author list includes participants in the events (e.g., Matiyasevich) and that the narrative relies partly on Davis's own recollections ([31], [39], [41]) and on an insider-edited volume ([78]); however, these serve as primary-source testimony about Davis's intellectual development, and the paper's evaluative claim that logic unified Davis's career is an interpretation of that testimony rather than a result forced by construction. The DPRM theorem is presented as a historical mathematical fact with independent literature support (e.g., [73], [74], [76], [60]), and the statement that 'One cannot overestimate the role played by Davis in resolving Hilbert's Tenth Problem' is an attribution, not an equation or fitted prediction. No Eq. X is shown to equal Eq. Y by construction, no fitted parameter is renamed as a prediction, and no load-bearing argument reduces to a self-citation chain. The paper is therefore self-contained as a historical overview, and no circularity is present.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no new parameters or entities; its content is wholly derivative of prior literature and personal recollections. The main epistemic burden is the trustworthiness of the insider account, which is not independently audited.

assumptions (3)
  • domain assumption The cited historical documents, letters, and personal recollections accurately represent the events described.
    The paper's historical narrative in Sections 2-4 relies on documents such as Robinson's letter [31] and recollections by the authors and Davis himself; if these are inaccurate or selectively quoted, the narrative is unreliable.
  • standard math Standard results of computability theory and number theory (e.g., recursive enumerability, Diophantine sets) are correct and can be used without proof.
    The paper invokes Davis normal form, DPRM theorem, and related results as established facts; these are external accepted results.
  • ad hoc to paper The authors' dual role as participants and historians does not systematically bias the selection of facts or their interpretation.
    Several authors including Matiyasevich, Omodeo, and Policriti are central figures in the narrative; the paper does not disclose how this insider status was controlled for, making objectivity an untested presumption.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Martin Davis: An Overview of his Work in Logic, Computer Science, and Philosophy." pith.science (2026). https://pith.science/paper/SC5MJY7Q

@misc{pith2026250608588,
  author       = {Pith},
  title        = {Pith review of: Martin Davis: An Overview of his Work in Logic, Computer Science, and Philosophy},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SC5MJY7Q}},
  note         = {Machine review of arXiv:2506.08588}
}
read the original abstract

In his autobiographic essay written in 1999, ``From logic to computer science and back'', Martin David Davis (3/8/1928--1/1/2023) indicated that he viewed himself as a logician \emph{and} a computer scientist. He expanded the essay in 2016 and expressed a new perspective through a changed title, ``My life as a logician''. He points out that logic was the unifying theme underlying his scientific career. Our paper attempts to provide a consistent vision that illuminates Davis' successive contributions leading to his landmark writings on computability, unsolvable problems, automated reasoning, as well as the history and philosophy of computing.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

97 extracted references · 74 canonical work pages

  1. [31]

    Foreword to the English translation of [74], pages xiii–xvii

    Martin Davis. Foreword to the English translation of [74], pages xiii–xvii. The MIT Press,

    work page

  2. [1]

    Diophantine complexity

    Leonard Adleman and Kenneth Manders. Diophantine complexity. In17th Annual IEEE Symposium on Foundations of Computer Science, pages 81–88, New York, 1976.doi:10. 1109/SFCS.1976.13

    1976

  3. [2]

    Rank stability in quadratic extensions and Hilbert's tenth problem for the ring of integers of a number field

    Levent Alpöge, Manjul Bhargava, Wei Ho, and Ari Shnidman. Rank stability in quadratic extensions and Hilbert’s tenth problem for the ring of integers of a number field, 2025. URL: arxiv.org/abs/2501.18774,arXiv:2501.18774

    work page Pith review arXiv 2025

  4. [3]

    IOS Press, second edition, 2021.doi:10.3233/FAIA336

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors.Handbook of Satisfi- ability, volume 336 ofFrontiers in Artificial Intelligence and Applications. IOS Press, second edition, 2021.doi:10.3233/FAIA336

    doi:10.3233/faia336 2021

  5. [4]

    Review: Martin Davis, Applied nonstandard analysis, and K

    Andreas Blass. Review: Martin Davis, Applied nonstandard analysis, and K. D. Stroyan and W. A. J. Luxemburg, Introduction to the theory of infinitesimals, and H. Jerome Keisler, Foundations of infinitesimal calculus.Bull. Amer. Math. Soc., 84(1):34–41, 1978. URL: projecteuclid.org/euclid.bams/1183540371

    work page arXiv 1978

  6. [5]

    A machine-independent theory of the complexity of recursive functions.J

    Manuel Blum. A machine-independent theory of the complexity of recursive functions.J. ACM, 14(2):322–336, 1967.doi:10.1145/321386.321395. 20See for instance [63]. 15

    work page arXiv 1967

  7. [6]

    In Memory of Martin Davis

    Wesley Calvert, Valentina Harizanov, Eugenio G. Omodeo, Alberto Policriti, and Alexandra Shlapentokh. In memory of Martin Davis.Notices Amer. Math. Soc., 71(7), 2024. (A preprint with an extensive bibliography is available atarxiv.org/pdf/2401.10154).doi:10.1111/ cag.12933

    work page Pith review arXiv 2024

  8. [7]

    Omodeo, and Alberto Policriti

    Domenico Cantone, Eugenio G. Omodeo, and Alberto Policriti. Banishing ultrafilters from our consciousness. In Omodeo and Policriti [78], pages 255–283.doi:10.1007/ 978-3-319-41842-1

Show all 97 references
  1. [8]

    Theorem- provingbymatching

    ThomasJ.Chinlund, MartinDavis, PeterG.Hinman, andMalcolmDouglasMcIlroy. Theorem- provingbymatching. Technicalreport, BellTelephoneLaboratories, Incorporated, MurrayHill, New Jersey, 1964

    1964

  2. [9]

    Jack Copeland

    B. Jack Copeland. Narrow versus wide mechanism: Including a re-examination of Turing’s views on the mind-machine issue.The Journal of Philosophy, 97(1):5–32, 2000. URL:www. jstor.org/stable/2678472

    2000

  3. [10]

    Arithmetical problems and recursively enumerable predicates (abstract).J

    Martin Davis. Arithmetical problems and recursively enumerable predicates (abstract).J. Symbolic Logic, 15(1):77–78, 1950

    1950

  4. [11]

    PhD thesis, Princeton University, May 1950

    Martin Davis.On the theory of recursive unsolvability. PhD thesis, Princeton University, May 1950

    1950

  5. [12]

    Relatively recursive functions and the extended Kleene hierarchy

    Martin Davis. Relatively recursive functions and the extended Kleene hierarchy. InProceedings of the International Congress of Mathematicians(Harvard University, Cambridge, MA, August 30–September 6, 1950), volume 1, page 723. AMS, Providence, RI, 1952

    1950

  6. [13]

    Arithmetical problems and recursively enumerable predicates.J

    Martin Davis. Arithmetical problems and recursively enumerable predicates.J. Symbolic Logic, 18(1):33–41, 1953. Russian transl. in [72, pp. 15–22]

    1953

  7. [14]

    McGraw-Hill, New York, 1958

    Martin Davis.Computability and Unsolvability. McGraw-Hill, New York, 1958. Reprinted with an additional appendix, Dover 1983. Italian translation [22]. Japanese translation [16]

    1958

  8. [15]

    Eliminating the irrelevant from mechanical proofs

    Martin Davis. Eliminating the irrelevant from mechanical proofs. InProc. Symp. Appl. Math., volume 15, pages 15–30, Providence, RI, 1963. AMS. (Reprinted in [92, pp. 315–330]; Russian transl. in [64, pp. 160–179]

    1963

  9. [16]

    Modern Science Selection

    Martin Davis.Theory of Computation. Modern Science Selection. Iwanami, Tokio, 1966. Japanese translation of [14]: Shigeru Watanabe

    1966

  10. [17]

    One equation to rule them all.Transactions of the New York Academy of Sciences.Series II, 30(6):766–773, 1968

    Martin Davis. One equation to rule them all.Transactions of the New York Academy of Sciences.Series II, 30(6):766–773, 1968

    1968

  11. [18]

    An explicit Diophantine definition of the exponential function.Comm

    Martin Davis. An explicit Diophantine definition of the exponential function.Comm. Pure Appl. Math., XXIV(2):137–145, 1971

    1971

  12. [19]

    On the number of solutions of Diophantine equations.Proc

    Martin Davis. On the number of solutions of Diophantine equations.Proc. Amer. Math. Soc., 35(2):552–554, 1972

    1972

  13. [20]

    Hilbert’s tenth problem is unsolvable.Amer

    Martin Davis. Hilbert’s tenth problem is unsolvable.Amer. Math. Monthly, 80(3):233–269,

  14. [21]

    Speed-up theorems and Diophantine equations

    Martin Davis. Speed-up theorems and Diophantine equations. In Randall Rustin, editor, Courant Computer Science Symposium 7: Computational Complexity, pages 87–95. Algorith- mics Press, Inc., New York, NY, 1973

    1973

  15. [22]

    Introduzione alla teoria della computabilità e alla teoria delle funzioni ricorsive

    Martin Davis.Computabilità e Insolubilità. Introduzione alla teoria della computabilità e alla teoria delle funzioni ricorsive. Collana di Epistemologia diretta da Evandro Agazzi. Edizioni Abete, Roma, 1975. Italian translation of [14]; foreword by Mariano Bianca (ed.)

    1975

  16. [23]

    John Wiley & Sons, Inc., 1977

    Martin Davis.Applied nonstandard analysis. John Wiley & Sons, Inc., 1977. Reprinted with corrections Dover, 2005. Russian translation, Publishing house “Mir”, Moscow 1980. Japanese translation 1977

    1977

  17. [24]

    Unsolvable problems

    Martin Davis. Unsolvable problems. In Jon Barwise, editor,Handbook of Mathematical Logic, pages 567–594. North-Holland, Amsterdam, 1977

    1977

  18. [25]

    The mathematics of non-monotonic reasoning.Artif

    Martin Davis. The mathematics of non-monotonic reasoning.Artif. Intell., 13(1-2):73–80, 1980

    1980

  19. [26]

    Obvious logical inferences

    Martin Davis. Obvious logical inferences. InProceedings of the 7th IJCAIVolume 1, pages 530–531, San Francisco, CA, USA, 1981. Morgan Kaufmann Publishers Inc

    1981

  20. [27]

    Why Gödel didn’t have Church’s thesis.Information and Control, 54(1/2):3–24, 1982

    Martin Davis. Why Gödel didn’t have Church’s thesis.Information and Control, 54(1/2):3–24, 1982

    1982

  21. [28]

    The prehistory and early history of Automated Deduction

    Martin Davis. The prehistory and early history of Automated Deduction. In Siekmann and Wrightson [92], pages 1–28

  22. [29]

    Is mathematical insight algorithmic?Behavioral and Brain Sciences, 13(4):659– 660, 1990

    Martin Davis. Is mathematical insight algorithmic?Behavioral and Brain Sciences, 13(4):659– 660, 1990

    1990

  23. [30]

    How subtle is Gödel’s theorem? More on Roger Penrose.Behavioral and Brain Sciences, 16:611–612, 9 1993

    Martin Davis. How subtle is Gödel’s theorem? More on Roger Penrose.Behavioral and Brain Sciences, 16:611–612, 9 1993. URL:journals.cambridge.org/article_S0140525X00031915, doi:10.1017/S0140525X00031915

    1993 doi

  24. [32]

    Martin Davis. Emil L. Post: His life and work. In Martin Davis, editor,Solvability, Provability, Definability: The Collected Works of Emil L. Post, pages xi–xxviii. Birkhäuser, Boston, Basel, Berlin, 1994

    1994

  25. [33]

    From logic to computer science and back

    Martin Davis. From logic to computer science and back. In Cristian S. Calude, editor,People and ideas in theoretical computer science, Discrete Mathematics and Theoretical Computer Science, pages 53–85. Springer-Verlag, Singapore, 1999

    1999

  26. [34]

    Martin Davis.The Universal Computer: The Road from Leibniz to Turing. W.W. Norton,

  27. [35]

    The myth of hypercomputation

    Martin Davis. The myth of hypercomputation. In Christof Teuscher, editor,Alan Turing: Life and Legacy of a Great Thinker, pages 195–211. Springer/Berlin/ Heidelberg, 2004.doi: 10.1007/978-3-662-05642-4_8. 17

    2004 doi

  28. [36]

    Why there is no such discipline as hypercomputation.Appl

    Martin Davis. Why there is no such discipline as hypercomputation.Appl. Math. Comput., 178(1):4–7, 2006. (Special issue on Hypercomputation, edited by F. A. Doria and J. F. Costa)

    2006

  29. [37]

    Representation theorems for r.e

    Martin Davis. Representation theorems for r.e. sets and a conjecture related to Poonen’s larges subring ofQ.Zapiski Nauchnykh Seminarov Peterburgskogo Otdeleniya Matematicheskogo In- stituta im. V.A.Steklova RAN (POMI), 377:50–54, 2010. Reproduced as [38]

    2010

  30. [38]

    Representation theorems for recursively enumerable sets and a conjecture related to Poonen’s large subring ofQ.J

    Martin Davis. Representation theorems for recursively enumerable sets and a conjecture related to Poonen’s large subring ofQ.J. Math. Sci. (N.Y.), 171(6):728–730, 2010. Reproduction of [37]

    2010

  31. [41]

    Seventy years of computer science

    Martin Davis. Seventy years of computer science. In Andreas Blass, Patrick Cégielski, Nachum Dershowitz, Manfred Droste, and Bernd Finkbeiner, editors,Fields of Logic and Computation III - Essays Dedicated to Yuri Gurevich on the Occasion of His 80th Birth- day, volume 12180 o...

    2020 doi

  32. [42]

    A free variable version of the first-order predicate calculus

    Martin Davis and Ronald Fechter. A free variable version of the first-order predicate calculus. J. Logic Comput., 1(4):431–451, 1991

    1991

  33. [43]

    Nonstandard analysis.Scientific American, 226:78–86, 1972

    Martin Davis and Reuben Hersh. Nonstandard analysis.Scientific American, 226:78–86, 1972

    1972

  34. [44]

    A machine program for theorem- proving

    Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem- proving. Technical Report AFOSR 819, IMM-NYU 288, New York University, Institute of Mathematical Sciences, June 1961

    1961

  35. [45]

    Loveland

    Martin Davis, George Logemann, and Donald W. Loveland. A machine program for theorem- proving.Commun. ACM, 5(7):394–397, 1962. Reprinted in [92, pp. 267–270]

    1962

  36. [46]

    Hilbert’s tenth problem

    Martin Davis, Yuri Matijasevič, and Julia Robinson. Hilbert’s tenth problem. Diophantine equations: positive aspects of a negative solution. In Felix E. Browder, editor,Mathematical Developments Arising From Hilbert Problems, volume 28 ofProc. Sympos. Pure Math., pages 323–354...

    1976

  37. [47]

    Feasible computational methods in the propositional cal- culus

    Martin Davis and Hilary Putnam. Feasible computational methods in the propositional cal- culus. Technical report, Rensselaer Polytechnic Institute, Research Division, Troy, New York, October 1958. Reprinted in [78, pp. 373–408]

    1958

  38. [48]

    Reductions of Hilbert’s tenth problem.J

    Martin Davis and Hilary Putnam. Reductions of Hilbert’s tenth problem.J. Symbolic Logic, 23(2):183–187, 1958. Russian transl. in [72, pp. 49–53]

    1958

  39. [49]

    A computational proof procedure; Axioms for number theory; Research on Hilbert’s Tenth Problem

    Martin Davis and Hilary Putnam. A computational proof procedure; Axioms for number theory; Research on Hilbert’s Tenth Problem. Technical Report AFOSR TR59-124, U.S. Air Force, October 1959. 18

    1959

  40. [50]

    A computing procedure for quantification theory.J

    Martin Davis and Hilary Putnam. A computing procedure for quantification theory.J. ACM, 7(3):201–215, 1960. Preprinted as [49, Part I]; reprinted in [92, pp. 125–139]

    1960

  41. [51]

    The decision problem for exponential Diophantine equations.Ann

    Martin Davis, Hilary Putnam, and Julia Robinson. The decision problem for exponential Diophantine equations.Ann. of Math. (2), 74(3):425–436, 1961. Reprinted in [87, pp. 77–88]. Russian transl. in [72, pp. 69–79]

    1961

  42. [52]

    Schwartz

    Martin Davis and Jacob T. Schwartz. Metamathematical extensibility for theorem verifiers and proof-checkers.Comput. Math. Appl., 5:217–230, 1979

    1979

  43. [53]

    Conceptual Confluence in 1936: Post and Turing

    Martin Davis and Wilfried Sieg. Conceptual Confluence in 1936: Post and Turing. In Giovanni Sommaruga and Thomas Strahm, editors,Turing’s Revolution. The impact of his ideas about Computability, pages 3–27. Birkhäuser, Basel, 2016

    1936

  44. [54]

    Weyuker.Computability, Complexity, and Languages

    Martin Davis, Ron Sigal, and Elaine J. Weyuker.Computability, Complexity, and Languages. Fundamentals of Theoretical Computer Science. Computer Science ad scientific computing. Academic Press, 2nd edition, 1994

    1994

  45. [55]

    Fundamentals of Theoretical Computer Science

    MartinDavisandElaineJ.Weyuker.Computability, Complexity, and Languages. Fundamentals of Theoretical Computer Science. Computer science and applied mathematics. Academic Press,

  46. [56]

    Daylight

    Edgar G. Daylight. A Turing tale.Communications of the ACM, 57(10):36–38, 2014

    2014

  47. [57]

    Daylight

    Liesbeth De Mol, Bullynck Maarten, and Edgar G. Daylight. Less is more in the fifties: Encounters between logical minimalism and computer design during the 1950s.IEEE Annals of the History of Computing, 40(1):19–45, 2018

    2018

  48. [58]

    The confluence of ideas in 1936

    Robin Gandy. The confluence of ideas in 1936. In Rolf Herken, editor,The Universal Turing machine, pages 55–111. Oxford University Press, Oxford, 1988

    1936

  49. [59]

    Paul C. Gilmore. A proof method for quantification theory: Its justification and realization. IBM Journal of Research and Development, 4(1):28–35, 1960.doi:10.1147/rd.41.0028

    1960 doi

  50. [60]

    The primes contain arbitrarily long arithmetic progressions.Ann

    Ben Green and Terence Tao. The primes contain arbitrarily long arithmetic progressions.Ann. of Math., 167:481–547, 2008.doi:10.4007/annals.2008.167.481

    2008 doi

  51. [61]

    Mathematische Probleme

    David Hilbert. Mathematische Probleme. Vortrag, gehalten auf dem internationalen Mathematiker-Kongreß zu Paris 1900.Nachrichten von der Königliche Gesellschaft der Wis- senschaften zu Göttingen, pages 253–297, 1900. (Translated as [62])

    1900

  52. [62]

    Mathematical Problems

    David Hilbert. Mathematical Problems. Lecture delivered before the International Congress of Mathematicians at Paris in 1900.Bulletin of the American Mathematical Society, 8:437–479, 1901-1902

    1900

  53. [63]

    Interview with Martin Davis.Notices Amer

    Allyn Jackson. Interview with Martin Davis.Notices Amer. Math. Soc., 55(5):560–571, 2008. doi:10.1090/noti457. [64]Kiberneticheskiy sbornik.Novaya seriya, 7. Publishing house “Mir”, Moscow, 1970

    2008 doi

  54. [65]

    Stephen C. Kleene. Origins of recursive function theory.IEEE Ann. Hist. Comput., 3(1):52–67, 1981.doi:10.1109/MAHC.1981.10004

    1981

  55. [66]

    Stephen Cole Kleene.Introduction to Metamathematics. P. Noordhoff N.V., Groningen, 1952. 19

    1952

  56. [67]

    Hilbert’s tenth problem via additive combinatorics, 2024

    Peter Koymans and Carlo Pagano. Hilbert’s tenth problem via additive combinatorics, 2024. URL=arxiv.org/abs/2412.01768.arXiv:2412.01768

    2024

  57. [69]

    Michael S. Mahoney. The history of computing in the history of technology.Annals of the History of Computing, 10(2):113–125, 1988

    1988

  58. [70]

    Mal’tsev

    Anatoly I. Mal’tsev. O nekotorykh pogranichnykh voprosakh algebry i logiki. InTrudy Mezh- dunarodnogo Kongressa Matematikov, pages 217–231, Moscow, 1968. Publishing house “Mir”

    1968

  59. [71]

    Almqvist & Wikseil, Stockholm, 1970

    Per Martin-Löf.Notes on Constructive Mathematics. Almqvist & Wikseil, Stockholm, 1970. [72]Matematika,8(5). Publishing house “Mir”, Moscow, 1964. URL: www.mathnet.ru/php/journal.phtml?jrnid=mat&option_lang=eng

    1970

  60. [73]

    Matiyasevich

    Yuri V. Matiyasevich. Diofantovost’ perechislimykh mnozhestv.Doklady Akademii Nauk SSSR, 191(2):279–282, 1970. (Russian. English translation by A. Doohovskoy as Ju. V. Matijasevič, Enumerable sets are Diophantine,Soviet Mathematics. Doklady, 11(3):354–358, 1970; Correc- tion, ...

    1970

  61. [74]

    Matiyasevich.Desyataya Problema Gilberta

    Yuri V. Matiyasevich.Desyataya Problema Gilberta. Fizmatlit, Moscow, 1993. English trans- lation:Hilbert’s Tenth problem. The MIT Press, Cambridge (MA) and London, 1993. French translation:Le dixième Problème de Hilbert: son indécidabilité, Masson, ParisMilanBarcelone,

    1993

  62. [76]

    Ram Murty and Brandon Fodden.Hilbert’s tenth problem

    M. Ram Murty and Brandon Fodden.Hilbert’s tenth problem. An introduction to logic, number theory, and computability, volume 88 ofStud. Math. Libr.Providence, RI: American Mathe- matical Society (AMS), 2019.doi:10.1090/stml/088

    2019 doi

  63. [77]

    Eugenio G. Omodeo. The Linked Conjunct method for automatic deduction and related search techniques.Comput. Math. Appl., 8(3):185–203, 1982

    1982

  64. [78]

    Omodeo and Alberto Policriti, editors.Martin Davis on Computability, Computa- tional Logic, and Mathematical Foundations, volume 10 ofOutstanding Contributions to Logic

    Eugenio G. Omodeo and Alberto Policriti, editors.Martin Davis on Computability, Computa- tional Logic, and Mathematical Foundations, volume 10 ofOutstanding Contributions to Logic. Springer, 2016.doi:10.1007/978-3-319-41842-1

    2016 doi

  65. [79]

    Oxford University Press, 1989

    RogerPenrose.The emperor’s new mind: Concerning computers, minds and the laws of physics. Oxford University Press, 1989. URL:www.worldcat.org/oclc/19724273

    1989

  66. [80]

    Oxford University Press, 1994

    Roger Penrose.Shadows of the mind: A search for the missing science of consciousness. Oxford University Press, 1994

    1994

  67. [81]

    Emil L. Post. Formal reductions of the general combinatorial decision problem.American Journal of Mathematics, 65(2):197–215, 1943

    1943

  68. [82]

    Emil L. Post. Formal reductions of the general combinatorial decision problem.American J. Math., 65:197–215, 1943. 20

    1943

  69. [83]

    Emil L. Post. Recursively enumerable sets of positive integers and their decision problems. Bulletin of the American Mathematical Society, 50(5):284–316, 1944

    1944

  70. [84]

    A mechanical proof procedure and its real- ization in an electronic computer.J

    Dag Prawitz, Håkan Prawitz, and Neri Voghera. A mechanical proof procedure and its real- ization in an electronic computer.J. ACM, 7(2):102–128, 1960

    1960

  71. [85]

    MAA Spectrum

    Constance Reid.Julia: A life in mathematics. MAA Spectrum. Mathematical Association of America, Washington, DC, 1996. With contributions by L. Gaal, M. Davis and Yu. Matijase- vich. MR:1418864. Zbl:0868.01020. Russian translation: [86]

    1996

  72. [86]

    Obrazovatelnye proekty

    Konstantsiya Rid.Dzhuliya. Zhizn v matematike. Publishing house “Obrazovatelnye proekty” (“Educational Projects”), St.Petersburg, 2023. Translation of [85], 160 pp

    2023

  73. [87]

    AMS, Providence, RI, 1996

    Julia Robinson.The collected works of Julia Robinson, volume 6 ofCollected Works. AMS, Providence, RI, 1996. ISBN 0-8218-0575-4. With an introduction by Constance Reid. Edited and with a foreword by Solomon Feferman. xliv+338 pp

    1996

  74. [88]

    Robinson

    Raphael M. Robinson. Arithmetical representation of recursively enumerable sets.J. Symbolic Logic, 21(2):162–186, 1956.doi:10.2307/2269027

    1956 doi

  75. [89]

    Sacks, editor.Mathematical Logic in the 20th Century

    Gerald E. Sacks, editor.Mathematical Logic in the 20th Century. Singapore University Press, Singapore; World Scientific Publishing Co., Inc., River Edge, NJ, 2003

    2003

  76. [90]

    Step by recursive step: Church’s analysis of effective calculability.Bull

    Wilfried Sieg. Step by recursive step: Church’s analysis of effective calculability.Bull. Symb. Log., 3(2):154–180, 1997.doi:10.2307/421012

    1997 doi

  77. [91]

    Siegelmann.Neural networks and analog computation: Beyond the Turing limit

    Hava T. Siegelmann.Neural networks and analog computation: Beyond the Turing limit. Progress in theoretical computer science. Birkhäuser, 1999

    1999

  78. [92]

    Springer, Berlin, Heidelberg, 1983

    Jörg Siekmann and Graham Wrightson, editors.Automation of Reasoning 1: Classical Papers on Computational Logic 1957-1966. Springer, Berlin, Heidelberg, 1983

    1957

  79. [93]

    Amethodofpresentingthetheoryofalgorithmsandenumerablesets(inRus- sian).Trudy Matematicheskogo instituta im

    GrigoriS.Tseitin. Amethodofpresentingthetheoryofalgorithmsandenumerablesets(inRus- sian).Trudy Matematicheskogo instituta im. V. A. Steklova, 72:69–99, 1964. English translation in: Am. Math. Soc. Translat., II. Ser.99, 1–39 (1972).doi:10.1007/978-0-387-68546-5_4

    1972 doi

  80. [94]

    Alan M. Turing. On computable numbers, with an application to theEntscheidungsproblem. Proc. London Math. Soc., 2(42):230–265, 1936. Correction, ibid., (43):544-546, 1937

    1936

  81. [95]

    Alan M. Turing. The word problem in semi-groups with cancellation.Annals of Mathematics (2), 52:491–505, 1950. URL:turing.ecs.soton.ac.uk/browse.php/B/31

    1950

  82. [96]

    Alan M. Turing. Solvable and unsolvable problems.Science News (Penguin Books), 31:7–23, February 1954

    1954

  83. [97]

    Toward mechanical mathematics.IBM Journal of Research and Development, 4(1):2–22, 1960.doi:10.1147/rd.41.0002

    Hao Wang. Toward mechanical mathematics.IBM Journal of Research and Development, 4(1):2–22, 1960.doi:10.1147/rd.41.0002

    1960 doi

  84. [98]

    Webb.Mechanism, Mentalism and Metamathematics

    Judson C. Webb.Mechanism, Mentalism and Metamathematics. Reidel Publishing Company, Dordecht, 1980

    1980

  85. [99]

    David L. Yarmush. The Linked Conjunct and other algorithms for mechanical theorem-proving. Technical Report IMM 412, Courant Institute of Mathematical Sciences, New York University, July 1976. 21

    1976

  86. [1973]

    199–235]

    Reprinted with corrections as Appendix 2 of the Dover edition ofComputability and Unsolvability[14, pp. 199–235]. 16

  87. [1993]

    The collaboration in the United States

    Reproduced with small modifications under the title “The collaboration in the United States”, in [85, pp.91–97] and in its Russian translation [86, pp.109–115]

  88. [1995]

    URL: logic.pdmi.ras.ru/∼yumat/H10Pbook/

    Greek translation:To dekato provlima tou Hilbert, Euryalos editions, Athena, 2022. URL: logic.pdmi.ras.ru/∼yumat/H10Pbook/

    2022

  89. [2000]

    Turing Centenary Edition, CRC Press, Taylor & Francis 2012

    2012

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.