相关论文: A short proof of the Strong Normalization of Class…

In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easily proved, only one of them is usually established (and…

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proof of which…

In this note we will show how to get consistency for first order classical logic, in a purely syntactic way, without going through cut elimination. The procedure is very simple and it uses the calculus of structures in an essential way. It…

Je\v{r}\'abek showed that cuts in classical propositional logic proofs in deep inference can be eliminated in quasipolynomial time. The proof is indirect and it relies on a result of Atserias, Galesi and Pudl\'ak about monotone sequent…

In this paper we will see deductive systems for classical propositional and predicate logic in the calculus of structures. Like sequent systems, they have a cut rule which is admissible. In addition, they enjoy a top-down symmetry and some…

We show that if a theory R defined by a rewrite system is super-consistent, the classical sequent calculus modulo R enjoys the cut elimination property, which was an open question. For such theories it was already known that proofs strongly…

This paper investigates the proof-theoretic foundations of double negation introduction (DNI) and double negation elimination (DNE) in classical logic. By examining both sequent calculus and natural deduction, it is shown that these rules…

We prove that given two cut free nets of linear logic, by means of their relational interpretations one can: 1) first determine whether or not the net obtained by cutting the two nets is strongly normalizable 2) then (in case it is strongly…

In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi LK and LJ enjoy cut elimination. The property is less…

We present intersection type systems in the style of sequent calculus, modifying the systems that Valentini introduced to prove normalisation properties without using the reducibility method. Our systems are more natural than Valentini's…

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…

We present a simpler way than usual to deduce the completeness theorem for the second-oder classical logic from the first-order one. We also extend our method to the case of second-order intuitionistic logic.

We give an elementary and purely arithmetical proof of the strong normalization of Parigot's simply typed $\lambda\mu$-calculus.

We shall settle the completeness of some classical positive propositional calculi (positive propositional calculi in which the so-called Peirce's law holds) by resorting to a close adaptation of Kalmar's completeness proof procedure. First…

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…

Termination is a major question in both logic and computer science. In logic, termination is at the heart of proof theory where it is usually called strong normalization (of cut elimination). In computer science, termination has always been…

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…

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.…

In this paper, we present a propositional sequent calculus containing disjoint copies of classical and intuitionistic logics. We prove a cut-elimination theorem and we establish a relation between this system and linear logic.

We extend to natural deduction the approach of Linear Nested Sequents and of 2-sequents. Formulas are decorated with a spatial coordinate, which allows a formulation of formal systems in the original spirit of natural deduction -- only one…