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