Abstract
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.
| Original language | English (US) |
|---|---|
| Title of host publication | Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings |
| Pages | 295-310 |
| Number of pages | 16 |
| State | Published - Oct 15 2007 |
| Event | 21st International Conference on Automated Deduction, CADE-21 2007 - Bremen, Germany Duration: Jul 17 2007 → Jul 20 2007 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 4603 LNAI |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 21st International Conference on Automated Deduction, CADE-21 2007 |
|---|---|
| Country | Germany |
| City | Bremen |
| Period | 7/17/07 → 7/20/07 |
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Fingerprint Dive into the research topics of 'Semantic relevance axiom selection system'. Together they form a unique fingerprint.
Cite this
Sutcliffe, G., & Puzis, Y. (2007). Semantic relevance axiom selection system. In Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings (pp. 295-310). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4603 LNAI).