Conclusion

Achieved so far ...

• First systematic development of ATP verification
• Generic verifier for TPTP format derivations
• Incomplete, but better than the (global) status quo

Applications

• Verification of proofs in the TSTP
• Verification of software verification proofs
• Verification of CASC outputs

Things to do ...

• Completely verify Skolemization
• User level verification
  • Test problem characteristics, e.g., axiom satisfiability
  • Detect proof flab