Computers, Reasoning and Mathematical Practice

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Computer aided formal reasoning, mathematical assistants which check complex arguments and automated proofs of new and interesting mathematical results have been part of the dream of computational logic for many years. This dream is in part being realised by the success of endeavours such as the Mizar project [110], which has produced many volumes of formalised mathematics, and McCune’s recent proof of the Robbins conjecture [79], cited, along with autonomous vehicle guidance and the chess program Deep Blue, as one of the five most significant achievements of artificial intelligence [114]. Yet it is still the case that few mathematicians use such programs, and their impact outside certain specialised communities has been less than might have been hoped.
Original languageEnglish
Title of host publicationComputational Logic
PublisherSpringer
Pages301-346
Number of pages46
Publication statusPublished - 1999

Publication series

NameNATO ASI Series
Volume165

Fingerprint

Dive into the research topics of 'Computers, Reasoning and Mathematical Practice'. Together they form a unique fingerprint.

Cite this