Algorithmic introduction of quantified cuts

DOI10.1016/j.tcs.2014.05.018zbMath1393.03050arXiv1401.4330OpenAlexW1999259832MaRDI QIDQ402115

Giselle Reis, Daniel Weller, Alexander Leitsch, Stefan Hetzl

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)

Related Items (15)

Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses ⋮ The problem of \(\Pi_{2}\)-cut-introduction ⋮ On the Herbrand content of LK ⋮ On the generation of quantified lemmas ⋮ Algorithmic introduction of quantified cuts ⋮ On the compressibility of finite languages and formal proofs ⋮ Unnamed Item ⋮ Higher-order pattern generalization modulo equational theories ⋮ Herbrand's theorem as higher order recursion ⋮ System Description: GAPT 2.0 ⋮ Learning from Łukasiewicz and Meredith: investigations into proof structures ⋮ Complexity of translations from resolution to sequent calculus ⋮ Compressibility of Finite Languages by Grammars ⋮ On the cover complexity of finite languages ⋮ Inductive theorem proving based on tree grammars

Uses Software

• SMT-LIB
• TPTP
• HR
• IsaCoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the complexity of Boolean unification
• Algorithmic introduction of quantified cuts
• Conjecture synthesis for inductive theories
• Rigid tree automata and applications
• Automatic construction and verification of isotopy invariants
• Describing proofs by short tautologies
• Don't eliminate cut
• Proof theory. 2nd ed
• Automaticity. I: Properties of a measure of descriptional complexity
• Boolean unification - the story so far
• Untersuchungen über das logische Schliessen. I
• Productive use of failure in inductive proof
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• 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
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• Incorporating Tables into Proofs
• Rigid Tree Automata
• Lower Bounds on Herbrand's Theorem
• 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

This page was built for publication: Algorithmic introduction of quantified cuts