[FOM] "Geometrical ways of reasoning" and visual proofs
Peter Smith
ps218 at cam.ac.uk
Sun Nov 28 06:00:19 EST 2004
Those interested in this topic (which has come up again in the thread on
Shapiro on formal and natural languages) might find the following
intriguing:
Mateja Jamnik, Mathematical Reasoning with Diagrams (CSLI publications,
2001).
An attractively written and accessible short book (Jamnik is a computer
scientist, now in Cambridge). Here's the blurb from the CSLI website, which
will give you the flavour:
Theorems in automated theorem proving are usually proved by formal logical
proofs. However, there is a subset of problems which humans can prove by
the use of geometric operations on diagrams, so called diagrammatic proofs.
This book investigates and describes how such diagrammatic reasoning about
mathematical theorems can be automated.
Concrete, rather than general diagrams are used to prove particular
instances of a universal statement. The "inference steps" of a diagrammatic
proof are formulated in terms of geometric operations on the diagram. A
general schematic proof of the universal statement is induced from these
proof instances by means of the constructive omega-rule. Schematic proofs
are represented as recursive programs which, given a particular diagram,
return the proof for that diagram. It is necessary to reason about this
recursive program to show that it outputs a correct proof. One method of
confirming that the abstraction of the schematic proof from the proof
instances is sound is proving the correctness of schematic proofs in the
meta-theory of diagrams. The book presents an investigation of these ideas
and their implementation in the system, called Diamond.
Dr Peter Smith: Faculty of Philosophy, University of Cambridge
www.logicbook.net | www.godelbook.net
--
http://www.phil.cam.ac.uk/teaching_staff/Smith/LaTeX/
(for the "LaTeX for Logicians" page)
More information about the FOM
mailing list