The problem of \(\Pi_{2}\)-cut-introduction

DOI10.1016/j.tcs.2017.10.003zbMath1423.03240arXiv1611.08208OpenAlexW2558493267MaRDI QIDQ1680562

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

sequent calculusproof theoryautomated deductionlemma generationproof grammar

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)

Related Items (2)

On the generation of quantified lemmas ⋮ Herbrand's theorem as higher order recursion

Uses Software

• HR
• GAPT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semantics and proof-theory of depth bounded Boolean logics
• Algorithmic introduction of quantified cuts
• Proof theory. 2nd ed
• Untersuchungen über das logische Schliessen. I
• Productive use of failure in inductive proof
• System Description: GAPT 2.0
• Applying Tree Languages in Proof Theory
• Automated Proof Compression by Invention of New Definitions
• Atomic Cut Introduction by Resolution: Proof Structuring and Compression
• Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars
• Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Cut-Based Abduction
• Three models for the description of language
• The consistency of arithmetics

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