Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)

TL;DR

This paper explores proof structures inspired by historical logic work to improve automated deduction by identifying features like lemmas that guide proof search more effectively, leading to shorter proofs.

Contribution

It provides a formal reconstruction of historical proof methods and introduces novel lemma generation techniques to enhance automated theorem proving.

Findings

Identified global proof features that guide proof search.

Developed a formal framework based on historical logic work.

Demonstrated shorter proofs with new lemma generation methods.

Abstract

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 {\L}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.