Computer scientists and mathematicians in the U.S., Europe, and Israel discuss the use of mechanization and automation for checking mathematical proofs and theorems, which was pioneered by N.G. de Bruijn in the 1960s. In the first paper, de Bruijn himself uses his experience of automating mathematics to reason about the human mind. Other contributors discuss such topics as recent results in type theory and their relation to automath; the use of Hoare logic with explicit contexts for deriving correct programs; and termination in ACL2 using multiset relations. Annotation ©2004 Book News, Inc., Portland, OR (booknews.com)
N.G. de Bruijn was a well established mathematician before deciding in 1967 at the age of 49 to work on a new direction related to Automating Mathematics. In the 1960s he became fascinated by the new computer technology and decided to start the Automath project where he could check, with the help of the computer, the correctness of books on mathematics. Through his work on Automath de Bruijn started a revolution in using the computer for verification, and since, we have seen more and more proof-checking and theorem-proving systems. Automath was written in Algol 60 and implemented on the primitive computers of the sixties. Thirty years on, both technology and theory have evolved a lot leading to impressive new directions in using the computer for manipulating and checking mathematics. This volume is a collection of papers with a personal flavour. It consists of 11 articles which propose interesting variations to or examples of mechanising mathematics and illustrate differ developments in symbolic computation in the past 35 years. The first paper is by de Bruijn himself where he uses his experience of automating mathematics to reason about the human mind. After that a number of intriguing articles have been contributed by amongst others Henk Barendregt, who proposes a mathematical proof language between informal and formalised mathematics which helps make proof assistants more user friendly, and Robert Constable, explaining how Automath's telescopes, books and definitions compare to recent developments in computational type theory made by his Nuprl group. The volume further includes a strong argumentation by Arnon Avron that for automated reasoning, there is an interesting logic, somewhere strictly between first and second order logic, determined essentially by an analysis of transitive closure, yielding induction; and Murdoch Gabbay presenting an interesting generalisation of Fraenkel-Mostowski (FM) set theory within higher-order logic, and applying it to model Milner's p-calculus.
