Divvy: An ATP meta-system based on axiom relevance ordering

Alex Roederer, Yury Puzis, Geoffrey Sutcliffe

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

11 Citations (Scopus)

Abstract

This paper describes two syntactic relevance orderings on the axioms available for proving a given conjecture, and an ATP meta-system that uses the orderings to select axioms to use in proof attempts. The system has been evaluated, and the results show that it is effective.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages157-162
Number of pages6
Volume5663 LNAI
DOIs
StatePublished - 2009
Event22nd International Conference on Automated Deduction, CADE-22 - Montreal, QC, Canada
Duration: Aug 2 2009Aug 7 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5663 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other22nd International Conference on Automated Deduction, CADE-22
CountryCanada
CityMontreal, QC
Period8/2/098/7/09

Fingerprint

Adenosinetriphosphate
Syntactics
Axiom
Axioms
Relevance
Syntax

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Roederer, A., Puzis, Y., & Sutcliffe, G. (2009). Divvy: An ATP meta-system based on axiom relevance ordering. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5663 LNAI, pp. 157-162). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5663 LNAI). https://doi.org/10.1007/978-3-642-02959-2_13

Divvy : An ATP meta-system based on axiom relevance ordering. / Roederer, Alex; Puzis, Yury; Sutcliffe, Geoffrey.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5663 LNAI 2009. p. 157-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5663 LNAI).

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

Roederer, A, Puzis, Y & Sutcliffe, G 2009, Divvy: An ATP meta-system based on axiom relevance ordering. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5663 LNAI, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5663 LNAI, pp. 157-162, 22nd International Conference on Automated Deduction, CADE-22, Montreal, QC, Canada, 8/2/09. https://doi.org/10.1007/978-3-642-02959-2_13
Roederer A, Puzis Y, Sutcliffe G. Divvy: An ATP meta-system based on axiom relevance ordering. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5663 LNAI. 2009. p. 157-162. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-02959-2_13
Roederer, Alex ; Puzis, Yury ; Sutcliffe, Geoffrey. / Divvy : An ATP meta-system based on axiom relevance ordering. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5663 LNAI 2009. pp. 157-162 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{5bc61dc2c8cd4d88a685cd52f347c2ee,
title = "Divvy: An ATP meta-system based on axiom relevance ordering",
abstract = "This paper describes two syntactic relevance orderings on the axioms available for proving a given conjecture, and an ATP meta-system that uses the orderings to select axioms to use in proof attempts. The system has been evaluated, and the results show that it is effective.",
author = "Alex Roederer and Yury Puzis and Geoffrey Sutcliffe",
year = "2009",
doi = "10.1007/978-3-642-02959-2_13",
language = "English (US)",
isbn = "3642029582",
volume = "5663 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "157--162",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - Divvy

T2 - An ATP meta-system based on axiom relevance ordering

AU - Roederer, Alex

AU - Puzis, Yury

AU - Sutcliffe, Geoffrey

PY - 2009

Y1 - 2009

N2 - This paper describes two syntactic relevance orderings on the axioms available for proving a given conjecture, and an ATP meta-system that uses the orderings to select axioms to use in proof attempts. The system has been evaluated, and the results show that it is effective.

AB - This paper describes two syntactic relevance orderings on the axioms available for proving a given conjecture, and an ATP meta-system that uses the orderings to select axioms to use in proof attempts. The system has been evaluated, and the results show that it is effective.

UR - http://www.scopus.com/inward/record.url?scp=69949162057&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=69949162057&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-02959-2_13

DO - 10.1007/978-3-642-02959-2_13

M3 - Conference contribution

AN - SCOPUS:69949162057

SN - 3642029582

SN - 9783642029585

VL - 5663 LNAI

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 157

EP - 162

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

ER -