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