[FOM] Standard Language of Euclid

[Peter LeFanu Lumsdaine]

On 26 Sep 2009, at 19:06, A. MANI wrote:

[snip]
> In the original language of Euclid it is not possible to remove the  
> schematic
> figures from the proof. It definitely possess a 'logic of diagrams'  
> component.
> It seems nobody has actually formalized it. 'School geometry' like  
> in some of
> the older British texts (Hall & Stevans for e.g) is in the language  
> you
> describe.

If I remember right, John Mumma looked at possible formalisations of  
Euclid's diagrammatic language in his PhD thesis, available at his  
website:
http://www.andrew.cmu.edu/user/jmumma/

Best,
-Peter.

-- 
Peter LeFanu Lumsdaine
Carnegie Mellon University