Other Projects
The TPTP and SystemOnTPTP
- Completed, but regular updates
The JJ Parser
- Parser for TPTP and TSTP files
- Implemented in C, to replace old Prolog code
- Extracts proof statistics
Meera's Performance Analyser
- Selects systems for SystemOnTPTP
- Uses performance data extracted from TSTP
- Improves previous SystemOnTPTP selection
Bernardo's Logical Voice
- FOL voice input
- Limited vocabulary, small grammar
- Based on IBM's ViaVoice
Homological Algebra
- A rich theory, "simple" theorems are hard for ATP
- Short Five Lemma
- Long Five Lemma and Snake Lemma