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

Created from the Publication Database of the Vienna University of Technology.