Semantic relevance axiom selection system

Geoff Sutcliffe, Yury Puzis

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

29 Scopus citations

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 languageEnglish (US)
Title of host publicationAutomated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
Pages295-310
Number of pages16
StatePublished - Oct 15 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

Other

Other21st International Conference on Automated Deduction, CADE-21 2007
CountryGermany
CityBremen
Period7/17/077/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).