SRASS - A Semantic Relevance Axiom Selection System

This paper 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.

• Type: Conference
• Year: 2007
• Where: CADE
• Authors: Geoff Sutcliffe, Yury Puzis
• Keywords: Automated Reasoning, CADE 2007, Conventional Automated Reasoning, Syntactic Relevance Measure