The Dashti Verifier

Semantic Proof Verification

• Two aspects
  • Check each inference is logical
  • Check input is copied correctly
• Technique
  • For each inference generate a proof obligation
    • Parents of step are the axioms
    • Conclusion of step is the conjecture
  • Submit to trustworthy ATP system
• Architecture
  
• Setting the limbo bar
• Cross verification

Proof Recontruction

• Splitting is a headache
• Reconstruction