Algorithmic introduction of quantified cuts
From MaRDI portal
Publication:402115
DOI10.1016/J.TCS.2014.05.018zbMATH Open1393.03050arXiv1401.4330OpenAlexW1999259832MaRDI QIDQ402115FDOQ402115
Authors: Stefan Hetzl, Alexander Leitsch, Giselle Reis, Daniel Weller 
Publication date: 27 August 2014
Published in: Theoretical Computer Science (Search for Journal in Brave)
Abstract: We describe a method for inverting Gentzen's cut-elimination in classical first-order logic. Our algorithm is based on first computign a compressed representation of the terms present in the cut-free proof and then cut-formulas that realize such a compression. Finally, a proof using these cut-formulas is constructed. This method allows an exponential compression of proof length. It can be applied to the output of automated theorem provers, which typically produce analytic proofs. An implementation is available on the web and described in this paper.
Full work available at URL: https://arxiv.org/abs/1401.4330
Recommendations
Cites Work
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- Title not available (Why is that?)
- Untersuchungen über das logische Schliessen. I
- Title not available (Why is that?)
- Title not available (Why is that?)
- Proof theory. 2nd ed
- Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
- Boolean unification - the story so far
- On the complexity of Boolean unification
- Rigid tree automata and applications
- Lower Bounds on Herbrand's Theorem
- Describing proofs by short tautologies
- Don't eliminate cut
- Automaticity. I: Properties of a measure of descriptional complexity
- Productive use of failure in inductive proof
- The automation of proof by mathematical induction
- Herbrand-confluence
- Applying tree languages in proof theory
- Towards Algorithmic Cut-Introduction
- On the complexity of proof deskolemization
- Automated proof compression by invention of new definitions
- Atomic cut introduction by resolution: proof structuring and compression
- Introducing Quantified Cuts in Logic with Equality
- Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
- Incorporating Tables into Proofs
- Rigid Tree Automata
- Title not available (Why is that?)
- Algorithmic introduction of quantified cuts
- Title not available (Why is that?)
- Title not available (Why is that?)
- Conjecture synthesis for inductive theories
- Title not available (Why is that?)
- Herbrand-confluence for cut elimination in classical first order logic
- MINIMAL RECOGNIZERS AND SYNTACTIC MONOIDS OF DR TREE LANGUAGES
- Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Automatic construction and verification of isotopy invariants
Cited In (19)
- Title not available (Why is that?)
- Herbrand's theorem as higher order recursion
- On the cover complexity of finite languages
- Algorithmic introduction of quantified cuts
- On the Herbrand content of LK
- Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses
- On the generation of quantified lemmas
- Title not available (Why is that?)
- System Description: GAPT 2.0
- Atomic cut introduction by resolution: proof structuring and compression
- Higher-order pattern generalization modulo equational theories
- Complexity of translations from resolution to sequent calculus
- Learning from Łukasiewicz and Meredith: investigations into proof structures
- Towards Algorithmic Cut-Introduction
- Compressibility of Finite Languages by Grammars
- The problem of \(\Pi_{2}\)-cut-introduction
- Title not available (Why is that?)
- On the compressibility of finite languages and formal proofs
- Inductive theorem proving based on tree grammars
Uses Software
This page was built for publication: Algorithmic introduction of quantified cuts
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q402115)
