Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
This work addresses a bottleneck in automated deduction for researchers and practitioners by providing incremental improvements in proof search guidance.
The paper tackles the problem of guiding automated proof search more effectively by identifying and studying global features like lemmas in proofs, based on historical work by Łukasiewicz and Meredith. It results in novel lemma generation methods that strengthen automated first-order provers, particularly improving their ability to find short proofs.
The material presented in this paper contributes to establishing a basis deemed essential for substantial progress in Automated Deduction. It identifies and studies global features in selected problems and their proofs which offer the potential of guiding proof search in a more direct way. The studied problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)". The features include the well-known concept of lemmas. For their elaboration both human and automated proofs of selected theorems are taken into a close comparative consideration. The study at the same time accounts for a coherent and comprehensive formal reconstruction of historical work by Łukasiewicz, Meredith and others. First experiments resulting from the study indicate novel ways of lemma generation to supplement automated first-order provers of various families, strengthening in particular their ability to find short proofs.