[FOM] Some Mathematical Case Studies in ProofPower-HOL

[Rob Arthan]

Dear All,

I have some case studies in formalising pure mathematics in  
ProofPower-HOL that may be of interest to FOM people. I have just added 
a document on group theory that deals with some general problems with 
practical formalisations of abstract algebraic theories.

The case studies are available on the web as PDF documents and in 
ProofPower source format at:

	http://www.lemma-one.com/ProofPower/examples/examples.html


I'd be very interested in any comments on these case studies, 
particularly on the group theory, which is where I have felt most 
strongly that the traditional explication of pure mathematics in set 
theory needs adjusting to work well in practice (formally or 
informally).

Regards,

Rob.