Investigations into Proof Structures

Christoph Wernhard, Wolfgang Bibel
2/14/2023
cs.LOcs.AI

No confident code implementation found for this paper.

Abstract

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description)

85% match2022

Lemmas: Generation, Selection, Application

84% match1 repo32023

Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

80% match2025

Diffusion-Proof: Recipe for Formal Theorem Proving Beyond Auto-Regressive Generation

78% match2026

Learning Formal Mathematics From Intrinsic Motivation

78% match1 repo362026

Mechanic: Sorrifier-Driven Formal Decomposition Workflow for Automated Theorem Proving

78% match2026

Cite this paper

@article{wernhard2023investigations,
  title  = {Investigations into Proof Structures},
  author = {Christoph Wernhard and Wolfgang Bibel},
  year   = {2023},
  eprint = {2304.12827},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2304.12827v3}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2304.12827.svg)](https://codeofpaper.com/paper/2304.12827)

Discussion