The Arrival of Automated Reasoning

Introduction

• ATP for the Novice
• The BCSK Logic (and the Axioms)
• Proof Structures
• The Starting Point

Discoveries in BCSK

• Dependent Axioms
• Proof Dependence
• Independent Axiom
• Short Proofs

Extending BCSK

• The BCSK+ Logic
• The SBPC Logic

Conclusion