zbMATH — the first resource for mathematics

On the shape of mathematical arguments. (English) Zbl 0705.68004
Lecture Notes in Computer Science, 445. Berlin etc.: Springer-Verlag. VIII, 181 p. DM 33.00 (1990).
The book deals with “human” theorem proving, and not with mechanical verification or mechanical theorem proving. The author does not address psychological questions like: “How do people find solutions“; she addresses more technical questions like: “How can proof design be guided by syntactic analysis of the demonstrandum”.
The book consists of two parts. The first one contains a mosaic of expositional essays, each of them dealing with one particular theorem; their proofs are used to illustrate what formalism is suitable to represent them in a form acceptable for computer scientists. Several technical criterions by which one argument can be objectively less streamlined than another are presented. Among the topics explored are proofs by cases, exploitation of symmetry, the problem of what to name, the exploitation of equivalence, proofs by calculation and their influence on the choice of notations, the degree of detail of proofs, and linearization of proofs. The second part consists of several more general chapters dealing in a more general setting with naming, clarity of exposition and notations.
Although the book is written as the “explanation-by-examples” it may be of interest for computer scientists dealing with program verification or mechanical theorem proving.
Reviewer: S.P.Yukna

68-02 Research exposition (monographs, survey articles) pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68Q60 Specification and verification (program logics, model checking, etc.)
03B35 Mechanization of proofs and logical operations
03F99 Proof theory and constructive mathematics
03-02 Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations