Abstract
"Large theory" problems in Automated Theorem Proving (ATP) have been defined as having many functions and predicates, and many axioms of which only a few are required for the proof of a theorem. One key to solving large theory problems is selecting a subset of the axioms that is adequate for finding a proof. The main contribution of this paper is metrics for evaluating axiom selection techniques without having to run an ATP system on the problem formed from the selected axioms and the problem's conjecture. This paper additionally presents three new axiom selection techniques. The new techniques, and the axiom selection in the Vampire ATP system, are evaluated using the metrics.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 63-75 |
| Number of pages | 13 |
| Journal | CEUR Workshop Proceedings |
| Volume | 2752 |
| State | Published - 2020 |
| Event | Joint of the 7th Workshop on Practical Aspects of Automated Reasoning and the 5th Satisfiability Checking and Symbolic Computation Workshop, PAAR+SC-Square 2020 - Virtual, Paris, France Duration: Jul 5 2020 → … |
Keywords
- Automated theorem proving
- Axiom selection
ASJC Scopus subject areas
- Computer Science(all)