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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Sutcliffe, G., & Puzis, Y. (2007). Semantic relevance axiom selection system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4603 LNAI, pp. 295–310). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_20
Mendeley helps you to discover research relevant for your work.