Algorithmic introduction of quantified cuts

DOI10.1016/J.TCS.2014.05.018zbMATH Open1393.03050OpenAlexW1999259832MaRDI 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)

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

zbMATH Keywords

first-order logicclassical logiccut-introductionproof compression

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

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.

Recommendations

• Towards Algorithmic Cut-Introduction
• The problem of \(\Pi_{2}\)-cut-introduction
• Cut Elimination In Situ
• Introducing quantified cuts in logic with equality
• Atomic cut introduction by resolution: proof structuring and compression

Cites work

• scientific article; zbMATH DE number 5909822 (Why is no real title available?)
• scientific article; zbMATH DE number 3668590 (Why is no real title available?)
• scientific article; zbMATH DE number 515726 (Why is no real title available?)
• scientific article; zbMATH DE number 627412 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 1747450 (Why is no real title available?)
• scientific article; zbMATH DE number 3032487 (Why is no real title available?)
• 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
• Automatic construction and verification of isotopy invariants
• Automaticity. I: Properties of a measure of descriptional complexity
• Boolean unification - the story so far
• Classification results in quasigroup and loop theory via a combination of automated reasoning tools.
• Conjecture synthesis for inductive theories
• Describing proofs by short tautologies
• Don't eliminate cut
• Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
• Herbrand-confluence
• Herbrand-confluence for cut elimination in classical first order logic
• Incorporating Tables into Proofs
• Introducing quantified cuts in logic with equality
• Lower Bounds on Herbrand's Theorem
• MINIMAL RECOGNIZERS AND SYNTACTIC MONOIDS OF DR TREE LANGUAGES
• On the complexity of Boolean unification
• On the complexity of proof deskolemization
• Productive use of failure in inductive proof
• Proof theory. 2nd ed
• Rigid Tree Automata
• Rigid tree automata and applications
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The automation of proof by mathematical induction
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Towards Algorithmic Cut-Introduction
• Untersuchungen über das logische Schliessen. I

Cited in

(20)

• Compressibility of Finite Languages by Grammars
• scientific article; zbMATH DE number 7447752 (Why is no real title available?)
• On the cover complexity of finite languages
• Higher-order pattern generalization modulo equational theories
• System description: GAPT 2.0
• Herbrand's theorem as higher order recursion
• Atomic cut introduction by resolution: proof structuring and compression
• Algorithmic introduction of quantified cuts
• scientific article; zbMATH DE number 2006630 (Why is no real title available?)
• Towards the compression of first-order resolution proofs by lowering unit clauses
• The problem of \(\Pi_{2}\)-cut-introduction
• Inductive theorem proving based on tree grammars
• On the generation of quantified lemmas
• Complexity of translations from resolution to sequent calculus
• Introducing quantified cuts in logic with equality
• Towards Algorithmic Cut-Introduction
• On the Herbrand content of LK
• Learning from Łukasiewicz and Meredith: investigations into proof structures
• On the compressibility of finite languages and formal proofs
• scientific article; zbMATH DE number 1086658 (Why is no real title available?)

Describes a project that uses

Uses Software

• SMT-LIB
• TPTP
• HR
• IsaCoSy

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)