Semantic relevance axiom selection system

Geoff Sutcliffe; Yury Puzis

doi:10.1007/978-3-540-73595-3_20

Semantic relevance axiom selection system

Geoff Sutcliffe, Yury Puzis

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings
Publisher	Springer Verlag
Pages	295-310
Number of pages	16
ISBN (Print)	3540735941, 9783540735946
DOIs	https://doi.org/10.1007/978-3-540-73595-3_20
State	Published - 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)

Access to Document

10.1007/978-3-540-73595-3_20

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). Springer Verlag. https://doi.org/10.1007/978-3-540-73595-3_20

Semantic relevance axiom selection system. / Sutcliffe, Geoff; Puzis, Yury.

Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Springer Verlag, 2007. p. 295-310 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4603 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Sutcliffe, G & Puzis, Y 2007, Semantic relevance axiom selection system. in Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4603 LNAI, Springer Verlag, pp. 295-310, 21st International Conference on Automated Deduction, CADE-21 2007, Bremen, Germany, 7/17/07. https://doi.org/10.1007/978-3-540-73595-3_20

Sutcliffe G, Puzis Y. Semantic relevance axiom selection system. In Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings. Springer Verlag. 2007. p. 295-310. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-73595-3_20

@inproceedings{de97895e053846a3b047a62234cd5da4,

title = "Semantic relevance axiom selection system",

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.",

author = "Geoff Sutcliffe and Yury Puzis",

year = "2007",

doi = "10.1007/978-3-540-73595-3_20",

language = "English (US)",

isbn = "3540735941",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "295--310",

booktitle = "Automated Deduction - CADE-21 - 21st International Conference on Automated Deduction, Proceedings",

note = "21st International Conference on Automated Deduction, CADE-21 2007 ; Conference date: 17-07-2007 Through 20-07-2007",

}

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 -