[FOM] "Geometrical ways of reasoning" and visual proofs

[Peter Smith]

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)