Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)
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.
Cite
@article{arxiv.2104.13645,
title = {Learning from {\L}ukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)},
author = {Christoph Wernhard and Wolfgang Bibel},
journal= {arXiv preprint arXiv:2104.13645},
year = {2021}
}