The STLP system (Short Theorems with Long Proofs) is designed to work
with finitely presented groups, and - initially at least - to apply the
ideas of Small Cancellation Theory to them.  

More specifically, Euler's formula on a van Kampen diagram should be 
used to define "curvature", with the intention of guiding the programs
to finding relators which, although short, do not have any short proof.

The system has not really got very far yet, but we are starting to 
work on it now (31.07.07).  We will see how far we can get!

Anyone interested in assisting with this fairly large project is very
welcome to email me (Richard) or anyone else on the team.

Richard Parker (richard@ukonline.co.uk)
Beth Holmes (p.e.holmes@dpmms.cam.ac.uk)
Christopher Parker (chris.parker2@gmail.com)

----------xxxxxxxxxx----------xxxxxxxxxx----------xxxxxxxxxx----------xx