Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Investigations into Proof Structures

Christoph Wernhard, Wolfgang Bibel

TL;DR

A novel formalism for the manipulation and analysis of proofs as objects in a global manner is introduced and 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.

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.

Investigations into Proof Structures

TL;DR

A novel formalism for the manipulation and analysis of proofs as objects in a global manner is introduced and 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.

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.
Paper Structure (63 sections, 15 theorems, 101 equations, 16 figures, 7 tables)

This paper contains 63 sections, 15 theorems, 101 equations, 16 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Relating Formal Human Proofs with ATP Proofs
  3. A Very Short Illustration of the Connection Method (CM)
  4. Łu-ka-sie-wicz's Shortest Single Axiom for the Implicational Fragment of Propositional Logic
  5. The First-Order ATP View on Detachment
  6. Comparing Proof Representations
  7. Condensed Detachment and a Formal Basis
  8. Notation
  9. Proof Structures: D-Terms
  10. Basic Definitions: Term View and Tree View
  11. Tree Size and Height
  12. DAG Representation and Compacted Size
  13. Comparing the Number of D-terms of a Given Size for Different Size Measures
  14. Node Labels for Proof Modularization
  15. Proof Structures, Formula Substitutions and Semantics
  16. ...and 48 more sections

Key Result

Proposition 17

For all terms $s$ whose variables are positional variables (Definition def-vpos) and for all positions $p$ it holds that

Figures (16)

  • Figure 1: A derivation in GS.
  • Figure 2: The connection proof for the Skolemized formula from Fig. \ref{['fig:briefcm:gsderivation']}.
  • Figure 3: The connection proof from Fig. \ref{['fig:briefcm:gs2derivation']} in matrix representation.
  • Figure 4: The first-order formula ŁDS along with its five unifiable connections.
  • Figure 5: A proof in different representations.
  • ...and 11 more figures

Theorems & Definitions (65)

  • Definition 1
  • Example 2
  • Example 3
  • Definition 4
  • Definition 5
  • Example 6
  • Definition 7
  • Example 8
  • Example 9
  • Example 10
  • ...and 55 more