Sign in
Back
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering
Book chapter   Peer reviewed

Divvy: An ATP Meta-system Based on Axiom Relevance Ordering

Alex Roederer, Yury Puzis and Geoff Sutcliffe
Automated Deduction – CADE-22, pp.157-162
Lecture Notes in Computer Science, Springer Berlin Heidelberg
2009
DOI: https://doi.org/10.1007/978-3-642-02959-2_13

Abstract

Latent Semantic Analysis Automate Reasoning Large Theory Automate Theorem Prove Relationship Strength
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.

Metrics

12 Record Views

Details