# Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)

arXiv: https://arxiv.org/abs/2104.13645 · HTML: https://mlsanity.com/paper/2104.13645/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 3 of its 48 references that are in the map.
- First posted on arXiv 28 Apr 2021.

## Builds on (most cited first, 3 of 3)

- [ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description)](https://mlsanity.com/paper/2002.05406/) (2020)
- [Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic](https://mlsanity.com/paper/2002.10892/) (2020)
- [Algorithmic Introduction of Quantified Cuts](https://mlsanity.com/paper/1401.4330/) (2014)

## Built on by (most cited first, 5 of 5)

- [CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)](https://mlsanity.com/paper/2207.08453/) (2022)
- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)
- [Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving](https://mlsanity.com/paper/2209.12592/) (2022)
- [Investigations into Proof Structures](https://mlsanity.com/paper/2304.12827/) (2023)
- [Range-Restricted Interpolation through Clausal Tableaux](https://mlsanity.com/paper/2306.03572/) (2023)

## Abstract (arXiv)

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 Lukasiewicz, 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.