Related papers: Algorithmic Introduction of Quantified Cuts

We describe an algorithmic method of proof compression based on the introduction of Pi_2-cuts into a cut-free LK-proof. The current approach is based on an inversion of Gentzen s cut-elimination method and extends former methods for…

Cut-elimination is the bedrock of proof theory. It is the algorithm that eliminates cuts from a sequent calculus proof that leads to cut-free calculi and applications. Cut-elimination applies to many logics irrespective of their semantics.…

Cut-introduction is a technique for structuring and compressing formal proofs. In this paper we generalize our cut-introduction method for the introduction of quantified lemmas of the form $\forall x.A$ (for quantifier-free $A$) to a method…

This paper is intended to provide an introduction to cut elimination which is accessible to a broad mathematical audience. Gentzen's cut elimination theorem is not as well known as it deserves to be, and it is tied to a lot of interesting…

This paper explores the connection between two central results in the proof theory of classical logic: Gentzen's cut-elimination for the sequent calculus and Herbrands "fundamental theorem". Starting from Miller's expansion-tree-proofs, a…

Cut-elimination theorems constitute one of the most important classes of theorems of proof theory. Since Gentzen's proof of the cut-elimination theorem for the system $\mathbf{LK}$, several other proofs have been proposed. Even though the…

Urban and Bierman introduced a calculus of proof terms for the sequent calculus LK with a strongly normalizing reduction relation. We extend this calculus to simply-typed higher-order logic with inferences for induction and equality, albeit…

Cut-elimination is the bedrock of proof theory with a multitude of applications from computational interpretations to proof analysis. It is also the starting point for important meta-theoretical investigations including decidability,…

The paper presents a cut-elimination procedure for intuitionistic propositional logic in which cut is eliminated directly, without introducing the multiple-cut rule mix, and in which pushing cut above contraction is one of the reduction…

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…

In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic…

We present a syntactic cut-elimination procedure for the alternation-free fragment of the modal mu-calculus. Cut reduction is carried out within a cyclic proof system, where proofs are finitely branching but may be non-wellfounded. The…

We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and…

Almost from the inception of Hilbert's program, foundational and structural efforts in proof theory have been directed towards the goal of clarifying the computational content of modern mathematical methods. This essay surveys various…

We consider modal logic extended with the well-known temporal operator 'eventually' and provide a cut-elimination procedure for a cyclic sequent calculus that captures this fragment. The work showcases an adaptation of the reductive…

Lorenzen's ``Algebraische und logistische Untersuchungen \"uber freie Verb\"ande'' appeared in 1951 in The journal of symbolic logic. These ``Investigations'' have immediately been recognised as a landmark in the history of infinitary proof…

Lorenzen's ``Algebraische und logistische Untersuchungen \"uber freie Verb\"ande'' appeared in 1951 in The Journal of Symbolic Logic. These ``Investigations'' have immediately been recognised as a landmark in the history of infinitary proof…

We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for…

We study cut elimination for a multifocused variant of full linear logic in the sequent calculus. The multifocused normal form of proofs yields problems that do not appear in a standard focused system, related to the constraints in grouping…

Resolution and superposition are common techniques which have seen widespread use with propositional and first-order logic in modern theorem provers. In these cases, resolution proof production is a key feature of such tools; however, the…