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

Alex Roederer, Yury Puzis, Geoff Sutcliffe

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

11 Scopus citations

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 publicationAutomated Deduction - CADE-22 - 22nd International Conference on Automated Deduction, Proceedings
Pages157-162
Number of pages6
DOIs
StatePublished - Sep 14 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)0302-9743
ISSN (Electronic)1611-3349

Other

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

    Fingerprint

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Roederer, A., Puzis, Y., & Sutcliffe, G. (2009). Divvy: An ATP meta-system based on axiom relevance ordering. In Automated Deduction - CADE-22 - 22nd International Conference on Automated Deduction, Proceedings (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