TY - GEN
T1 - Semantic relevance axiom selection system
AU - Sutcliffe, Geoff
AU - Puzis, Yury
PY - 2007
Y1 - 2007
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=35148824106&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=35148824106&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-73595-3_20
DO - 10.1007/978-3-540-73595-3_20
M3 - Conference contribution
AN - SCOPUS:35148824106
SN - 3540735941
SN - 9783540735946
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 295
EP - 310
BT - Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
PB - Springer Verlag
T2 - 21st International Conference on Automated Deduction, CADE-21 2007
Y2 - 17 July 2007 through 20 July 2007
ER -