# Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 58 references that are in the map.
- First posted on arXiv 26 Sep 2022.

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

- [The Role of Entropy in Guiding a Connection Prover](https://mlsanity.com/paper/2105.14706/) (2021)
- [Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (Extended Technical Report)](https://mlsanity.com/paper/2104.13138/) (2021)
- [Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic](https://mlsanity.com/paper/2002.10892/) (2020)
- [Learning from Lukasiewicz and Meredith: Investigations into Proof Structures (Extended Version)](https://mlsanity.com/paper/2104.13645/) (2021)
- [Craig Interpolation with Clausal First-Order Tableaux](https://mlsanity.com/paper/2008.03489/) (2020)
- [CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)](https://mlsanity.com/paper/2207.08453/) (2022)
- [Asymptotic Enumeration of Compacted Binary Trees of Bounded Right Height](https://mlsanity.com/paper/1703.10031/) (2017)
- [Combinators: A Centennial View](https://mlsanity.com/paper/2103.12811/) (2021)
- [A Bibliography of Combinators](https://mlsanity.com/paper/2106.11729/) (2021)

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

- [Lemmas: Generation, Selection, Application](https://mlsanity.com/paper/2303.05854/) (2023)
- [Investigations into Proof Structures](https://mlsanity.com/paper/2304.12827/) (2023)

## Abstract (arXiv)

Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these straightforwardly factor into shared subgraphs. To search for proofs, combinator terms can be enumerated, like clausal tableaux, interwoven with unification of formulas that are associated with nodes of the enumerated structures. To restrict the search space, the enumeration can be based on proof schemas defined as parameterized combinator terms. We introduce here this "combinator term as proof structure" approach to automated first-order proving, present an implementation and first experimental results. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method. It realizes features known from the connection structure calculus, which has not been implemented so far.