Title :
The automation of proof: a historical and sociological exploration
Author :
Mackenzie, Donald
Author_Institution :
Dept. of Sociol., Edinburgh Univ., UK
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
Keywords :
artificial intelligence; formal logic; history; mathematics computing; theorem proving; artificial intelligence; automatic theorem proving; computer history; computer program verification; deduction; hardware designs; historical; interactive theorem proving; mathematical logic; mathematical proofs; proof automation; sociological; Artificial intelligence; Computational modeling; Design automation; Hardware; History; Humans; Laboratories; Logic design; Machine intelligence; Mathematics;
Journal_Title :
Annals of the History of Computing, IEEE
