Subscribe
Issue No.03  Fall (1995 vol.17)
pp: 729
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/85.397057
ABSTRACT
<p>This article reviews the history of the use of computers to automate mathematical proofs. It identifies three broad strands of work: automatic theorem proving where the aim is to simulate human processes of deduction; automatic theorem proving where any resemblance to how humans deduce is considered to be irrelevant; and interactive theorem proving, where the proof is directly guided by a human being. The first strand has been underpinned by commitment to the goal of artificial intelligence; practitioners of the second strand have been drawn mainly from mathematical logic; and the third strand has been rooted primarily in the verification of computer programs and hardware designs.</p>
CITATION
Donald MacKenzie, "The Automation of Proof: A Historical and Sociological Exploration", IEEE Annals of the History of Computing, vol.17, no. 3, pp. 729, Fall 1995, doi:10.1109/85.397057
REFERENCES
