ProofWatch: Watchlist Guidance for Large Theories in E

  Zarathustra Goertzel, Jan Jakub, Stephan Schulz, Josef Urban


Watchlist (also hint list) is a mechanism that allows related proofs
to guide a proof search for a new conjecture. This mechanism has been
used with the Otter and Prover9 theorem provers, both for interactive
formalizations and for human-assisted proving of open conjectures in
small theories.  In this work we explore the use of watchlists in
large theories coming from first-order translations of large ITP
libraries, aiming at improving hammer-style automation by smarter
internal guidance of the ATP systems. In particular, we

(i) design watchlist-based clause evaluation heuristics inside the E
ATP system, and (ii) develop new proof guiding algorithms that load
many previous proofs inside the ATP and focus the proof search using a
dynamically updated notion of proof matching.  The methods are
evaluated on a large set of problems coming from the Mizar library,
showing significant improvement of E's standard portfolio of
strategies, and also of the previous best set of strategies invented
for Mizar by evolutionary methods.