Semantic Derivation Verification

Introduction

• What is ATP?
• ATP Proof Techniques
• Motivation for Verifying Derivations
• Verification Techniques (we don't use)
• Verification Techniques (we do use)

Semantic Verification

• Derivation DAGs
• Derived Formulae
• Leaf Formulae
• Explicitly Split Formulae
• Pseudo Split Formulae

Structural Verification

Verification in Action

• Implementation and Testing
• Trusting the Verifier
• Conclusion