Investigations into Proof Structures
This work addresses proof search efficiency in automated theorem proving, offering incremental improvements for generating shorter proofs in formal logic.
The paper tackles the problem of proof search in first-order logic by introducing a novel formalism for manipulating and analyzing proofs globally, applied to Łukasiewicz's problem, resulting in an automatically discovered proof that is much shorter than any previous proof.
We introduce and elaborate a novel formalism for the manipulation and analysis of proofs as objects in a global manner. In this first approach the formalism is restricted to first-order problems characterized by condensed detachment. It is applied in an exemplary manner to a coherent and comprehensive formal reconstruction and analysis of historical proofs of a widely-studied problem due to Łukasiewicz. The underlying approach opens the door towards new systematic ways of generating lemmas in the course of proof search to the effects of reducing the search effort and finding shorter proofs. Among the numerous reported experiments along this line, a proof of Łukasiewicz's problem was automatically discovered that is much shorter than any proof found before by man or machine.