Proof by refutation of a geometry theorem that is not universally true produces a Gröbner basis whose elements, called side polynomials, may be used to give inequations that can be added to the hypotheses to give a valid theorem. We show that (in a certain sense) all possible subsidiary conditions are implied by those obtained from the basis; that what we call the kind of truth of the theorem may be derived from the basis; and that the side polynomials may (...) be classified in a useful way. We analyse the relationship between side polynomials and kinds of truth, and we give a unified algorithmic treatment of side polynomials, with examples generated by an implementation. (shrink)

A detailed axiomatisation of diagrams (in affine geometry) is presented, which supports typing of geometric objects, calculation of geometric quantities and automated proof of theorems.

REVIEW OF: The Symbolic Species - The co-evolution of language and the human brain, by Terrence Deacon, Penguin, 527pp, 1997. -/- Terrence Deacon works at the interface between neurobiology, developmental biology and biological anthropology. He is ideally placed to bring together the insights of the very different sciences of palaeontology and physiology into the nature and origins of language. The pleasures of his book are in the detail, the expert knowledge that the author brings to bear, the lucidity of writing (...) that must at times be quite technical. -/- The reviewer sees a main inadequacy of the book in its cavalier treatment of language itself, and especially of what the author calls "Chomsky's Handstand". (shrink)

REVIEW OF: Automated Development of Fundamental Mathematical Theories by Art Quaife. (1992: Kluwer Academic Publishers) 271pp. Using the theorem prover OTTER Art Quaife has proved four hundred theorems of von Neumann-Bernays-Gödel set theory; twelve hundred theorems and definitions of elementary number theory; dozens of Euclidean geometry theorems; and Gödel's incompleteness theorems. It is an impressive achievement. To gauge its significance and to see what prospects it offers this review looks closely at the book and the proofs it presents.