The PGIP and PGML schema referred to throughout this thesis are given below. Updated versions may be available from http://proofgeneral.inf.ed.ac.uk/kit.