Evaluation of axiom selection techniques

Qinghua Liu, Zishi Wu, Zihao Wang, Geoff Sutcliffe

Research output: Contribution to journalConference articlepeer-review


"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 languageEnglish (US)
Pages (from-to)63-75
Number of pages13
JournalCEUR Workshop Proceedings
StatePublished - 2020
EventJoint 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 → …


  • Automated theorem proving
  • Axiom selection

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Evaluation of axiom selection techniques'. Together they form a unique fingerprint.

Cite this