Divvy: An ATP Meta-system
based on Axiom Relevance Ordering
Abstract
This presentation 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.