Semantic relevance axiom selection system

Geoff Sutcliffe, Yury Puzis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

32 Scopus citations


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 languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
PublisherSpringer Verlag
Number of pages16
ISBN (Print)3540735941, 9783540735946
StatePublished - 2007
Event21st International Conference on Automated Deduction, CADE-21 2007 - Bremen, Germany
Duration: Jul 17 2007Jul 20 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4603 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other21st International Conference on Automated Deduction, CADE-21 2007

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Semantic relevance axiom selection system'. Together they form a unique fingerprint.

Cite this