%0 Journal Article %1 mackenzie1995 %A Mackenzie, D. %D 1995 %J IEEE Annals of the History of Computing %K MIGHTREAD %N 3 %P 7-29 %R 10.1109/85.397057 %T The automation of proof: a historical and sociological exploration %U http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=397057 %V 17 %X 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

@article{mackenzie1995, 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}, added-at = {2007-04-11T23:05:04.000+0200}, author = {Mackenzie, D.}, biburl = {https://www.bibsonomy.org/bibtex/2a97ef137f0e0963249232f3595e876a8/mstrohm}, doi = {10.1109/85.397057}, interhash = {d5dc640ffe0c7bce2649ec2f58bca68d}, intrahash = {a97ef137f0e0963249232f3595e876a8}, issn = {1058-6180}, journal = {IEEE Annals of the History of Computing}, keywords = {MIGHTREAD}, number = 3, pages = {7-29}, timestamp = {2007-04-11T23:05:04.000+0200}, title = {The automation of proof: a historical and sociological exploration}, url = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=397057}, volume = 17, year = 1995 }