Algorithmic introduction of quantified cuts
From MaRDI portal
Publication:402115
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
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
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
