GDV - Semantic Derivation Verification

• Need to verify TPTP derivations
• Incompleteness, Soundness, Correctness
• Complexity and experience indicates bugs
• Other techniques (we don't use directly)

• Parents
• Cycles
• Refutations
• Constraints on splitting steps
• Use of assumptions

• Generate obligation for each formula (including leaves) in derivation
• Discharge using a trusted system (Otter!)
• Obligation determined by SZS status stored with each annotated formula

Verifying E's refutation of PUZ001+1 in SystemOnTSTP/GDV