Proving Hard Theorems in Rich Theories, Part II

Introduction

• What is ATP?
• What are "Rich Theories"?
• Approaches to Proving Hard Theorems
• Brute Force and Ignorance
• Subtlety and Intelligence

Measuring Relevance

• Background
• Direct Relevance
• Contextual Direct Relevance
• Variables
• Transitive Relevance
• Combining Predicate and Functor Relevance
• Evaluation

Axiom Selection

• Binary Search
• Combinations of Axioms
• Probabilistic Ordering
• Grouping by Relevance
• Evaluation

Lemma Selection

• Linear Addition and Replacement
• Recursive Approach
• Using Relevance
• Evaluation