The problem of _2-cut-introduction

DOI10.1016/J.TCS.2017.10.003MaRDI QIDQ1680562zbMATH OpenOpenAlexFDO

Authors Alexander Leitsch, Michael Peter Lettmann

Publication date 16 November 2017

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1611.08208

zbMATH Keywords

automated deductionlemma generationproof grammarproof theorysequent calculus

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07) Complexity of proofs (03F20)

Abstract: We describe an algorithmic method of proof compression based on the introduction of Pi_2-cuts into a cut-free LK-proof. The current approach is based on an inversion of Gentzen s cut-elimination method and extends former methods for introducing Pi_1-cuts. The Herbrand instances of a cut-free proof pi of a sequent S are described by a grammar G which encodes substitutions defined in the elimination of quantified cuts. We present an algorithm which, given a grammar G, constructs a Pi_2-cut formula A and a proof phi of S with one cut on A. It is shown that, by this algorithm, we can achieve an exponential proof compression.

Recommendations

• On the \(k\)-cut problem
• scientific article; zbMATH DE number 1506038
• The planar multiterminal cut problem
• Towards Algorithmic Cut-Introduction
• On the \((A,B)\)-slice problem
• The perfect matching cut problem revisited
• The perfect matching cut problem revisited
• A note on the problem of r disjoint (s, t)-cuts and some related issues
• scientific article; zbMATH DE number 3996512
• Cuts in undirected graphs. II

Cites work

• Algorithmic introduction of quantified cuts
• Applying tree languages in proof theory
• Atomic cut introduction by resolution: proof structuring and compression
• Automated proof compression by invention of new definitions
• Cut-Based Abduction
• Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
• Herbrand disjunctions, cut elimination and context-free tree grammars
• scientific article; zbMATH DE number 5909822 (Why is no real title available?)
• scientific article; zbMATH DE number 949290 (Why is no real title available?)
• scientific article; zbMATH DE number 7178366 (Why is no real title available?)
• Normal form transformations
• Productive use of failure in inductive proof
• Proof theory. 2nd ed
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Semantics and proof-theory of depth bounded Boolean logics
• System description: GAPT 2.0
• Tableaux and related methods
• The automation of proof by mathematical induction
• The consistency of arithmetics
• Three models for the description of language
• Untersuchungen über das logische Schliessen. I

Cited in

(5)

• Herbrand's theorem as higher order recursion
• On the generation of quantified lemmas
• Project presentation: algorithmic structuring and compression of proofs (ASCOP)
• Atomic cut introduction by resolution: proof structuring and compression
• Algorithmic introduction of quantified cuts

Describes a project that uses

Uses Software

• HR
• GAPT

This page was built for publication: The problem of \(\Pi_{2}\)-cut-introduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1680562)