[Back]

G. Reger, M. Suda:
"Measuring progress to predict success: Can a good proof strategy be evolved?";
Talk: AITP 2017 - The Second Conference on Artificial Intelligence and Theorem Proving, Obergurgl (invited); 2017-03-26 - 2017-03-30.

One of the main parameters of the superposition calculus employed by Automated Theorem
Provers (ATPs) is the simplification ordering, and the choice of an ordering can have a huge
impact on the success of a theorem proving attempt. However, it is difficult to choose a good
ordering in advance and ATPs typically provide only a few heuristical schemes for determining
an ordering from a large space of possibilities. The aim of this work is to establish to what
extent the space of possible orderings can be better utilised during the construction of new
successful proving strategies.
There is a well known principle in automated deduction which states that a strategy that
leads to a slowly growing search space will likely be more successful (at finding a proof in
reasonable time) than a strategy that leads to a rapidly growing one. We propose to employ
this principle and search for a strategy which, for a given problem, minimises the number of
derived clauses after a certain number of iterations of the saturation loop. Focusing on the
search for a good ordering as a simplifying restriction on the set of available strategies, we
experimentally investigate the practical potential of this idea.

Automated Theorem Provers, simplification orderings, proving strategies

http://publik.tuwien.ac.at/files/publik_264601.pdf