Semantic Proof Verification

Principle

• Check input is copied correctly
• Check each inference is logical
• For each inference generate a proof obligation
  • Parents of step are the axioms
  • Conclusion of step is the conjecture
• Submit to trustworthy ATP system

Implementation

• DV in perl
  • Reads TSTP format
  • Verifies with Otter
• DVDV in C
  • Uses the JJParser to read TSTP format
  • Verifies with SystemOnTPTP

Issues

• Proofs vs Refutations
• Satisfiability preserving transformations in refutations
• Setting the limbo bar
• Cross verification