SRASS
a Semantic Relevance Axiom Selection System
Abstract
This talk describes the design, implementation, and testing of a system for
selecting necessary axioms from a large set also containing superfluous
axioms, to obtain a proof of a conjecture.
The selection is determined by semantics of the axioms and conjecture,
ordered heuristically by a syntactic relevance measure.
The system is able to solve many problems that cannot be solved alone by the
underlying conventional automated reasoning system.