ProofCheck is a suite of Python scripts that aid an author using TeX, parse and check mathematical proofs. The checking program is essentially a classic rule-based program where in this case the rules are logical rules of inference.
The presentation consists of:
I. An introduction itemizing the various scripts and their functions: parsing, checking, renumbering, etc. II A data-flow diagram showing the external supporting files needed: the rules of inference file, a common notions file, etc. III. A description of the Proof markup syntax needed to enable checking. IV. A sample proof (of the fact that divisibility is transitive) showing both the TeX source file and the PDF output file. V. A comparison of ProofCheck with well-known programs such as Mizar and HOL.