SRASS
a Semantic Relevance Axiom Selection System

Introduction

• Motivation
• Background Concepts

Semantic Relevance Axiom Selection

• The Basic Process
• Exceptional Cases

The Extended Process

• Syntactic Relevance Ordering
• Efficient and Greedy Termination
• Incomplete Models
• Inadequate Models
• Last Gasp Selection
• Aggressive Selection
• Batch and Limited Selection
• Initial and Final Proof Attempts

Implementation and Evaluation

• Implementation
• Testing
• Results
• On the MPTP Challenge

Conclusion