ProofBot is an open-source, cross-platform proofwriting application which subscribes to the heuristics outlined in Gries and Schneider’s A Logical Approach to Discrete Math (LADM), Springer-Verlag, 1993. It was designed in particular as a tool for students of Pepperdine University’s Formal Methods and Discrete Structures courses.
A list of theorems from LADM as compiled by Prof. J. Stanley Warford can be found here.
To avoid the headache of writing platform-specific software, ProofBot was written using the Qt framework.
- Cross-platform printer support
- Saves each proof as a convenient little .txt file
- Quick and painless typesetting (and all typeset elements are just Unicode!)
- Elegant and non-intrusive syntax hilighting
- Expand list of recognized symbols
- Selective markdown support
- Included list of theorems (hopefully with auto-completion)