Browse Prior Art Database

The Automation of Proof: A Historical and Sociological Exploration

IP.com Disclosure Number: IPCOM000129890D
Original Publication Date: 1995-Sep-30
Included in the Prior Art Database: 2005-Oct-07

Publishing Venue

Software Patent Institute

Related People

DONALD MACKENZIE: AUTHOR [+2]

Abstract

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. Traditionally, the most important relationship of the computer to mathematics has been in the automation of calculation. Since the middle of the 1950s, however, another relationship has emerged: the automation of mathematical reasoning, especially the automation of mathematical proof. Originally intertwined with the emergence of the new field of artificial intelligence, the automation of proof has also spawned two important programming languages, Prolog and ML. It has provided crucial technical underpinnings for the attempt mathematically to verify the correctness of programs and hardware designs. It is beginning to contribute to mathematical research. The main aim of this article is to provide a history of the automation of proof that places its technical features in their wider intellectual and practical context. It builds upon the historical articles by Davis,' Was and Henschen,2 Loveland,3 and O'Leary,4 and complements Lolli's wide-ranging book.5 (The latter, unfortunately, is available only in Italian; my attention was drawn to it by a referee of the first draft of this article.)

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 3% of the total text.

Page 1 of 40

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Copyright ©; 1995 by the Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Used with permission.

The Automation of Proof: A Historical and Sociological Exploration

DONALD MACKENZIE

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.

Traditionally, the most important relationship of the computer to mathematics has been in the automation of calculation. Since the middle of the 1950s, however, another relationship has emerged: the automation of mathematical reasoning, especially the automation of mathematical proof. Originally intertwined with the emergence of the new field of artificial intelligence, the automation of proof has also spawned two important programming languages, Prolog and ML. It has provided crucial technical underpinnings for the attempt mathematically to verify the correctness of programs and hardware designs. It is beginning to contribute to mathematical research.

The main aim of this article is to provide a history of the automation of proof that places its technical features in their wider intellectual and practical context. It builds upon the historical articles by Davis,' Was and Henschen,2 Loveland,3 and O'Leary,4 and complements Lolli's wide-ranging book.5 (The latter, unfortunately, is available only in Italian; my attention was drawn to it by a referee of the first draft of this article.)

After this introduction comes a discussion of the first of the two main features of this intellectual context, that is, the development of ideas of proof in mathematics and logic prior to the advent of the digital computer, focusing on ideas that have both informed technically and framed conceptually the automation of mathematical reasoning. This section has no claim to either historical adequacy or sociological insight; it is essentially tutorial in nature, and readers confident of their understanding of this background can skip the section.

Then follows a section discussing the early automated theorem provers of the 1950s, and this brings in the second feature of intellectual context: the emergence of "artificial intelligence." The goal of much of the early automation of proof was explicitly to invent "a thinking machine" rather than a mere calculating machine, and success in the enterprise was seen as a...