Related papers: Confluence as a cut elimination property

In the recent past, the reduction-based and the model-based methods to prove cut elimination have converged, so that they now appear just as two sides of the same coin. This paper details some of the steps of this transformation.

We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating…

In this note we give a simple unifying proof of the undecidability of several diagrammatic properties of term rewriting systems that include: local confluence, strong confluence, diamond property, subcommutative property, and the existence…

We verify a confluence result for the rewriting calculus of the linear category introduced in our previous paper. Together with the termination result proved therein, the generalized coherence theorem for linear category is established.…

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

Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence…

We give a simple and direct proof that super-consistency implies the cut elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes…

We present two methods for proving confluence of left-linear term rewrite systems. One is hot-decreasingness, combining the parallel/development closedness theorems with rule labelling based on a terminating subsystem. The other is…

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has…

Deduction systems and graph rewriting systems are compared within a common categorical framework. This leads to an improved deduction method in diagrammatic logics.

Like termination, confluence is a central property of rewrite systems. Unlike for termination, however, there exists no known complexity hierarchy for confluence. In this paper we investigate whether the decreasing diagrams technique can be…

Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may…

We propose a functional description of rewriting systems where reduction rules are represented by linear maps called reduction operators. We show that reduction operators admit a lattice structure. Using this structure we define the notion…

We propose a functional description of rewriting systems on topological vector spaces. We introduce the topological confluence property as an approximation of the confluence property. Using a representation of linear topological rewriting…

This paper develops an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-elimination, and identity expansion. Although undecidable in general, these…

We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were…

Confluence of a nondeterministic program ensures a functional input-output relation, freeing the programmer from considering the actual scheduling strategy, and allowing optimized and perhaps parallel implementations. The more general…

This article describes the *Confluence Framework*, a novel framework for proving and disproving confluence using a divide-and-conquer modular strategy, and its implementation in CONFident. Using this approach, we are able to automatically…

In this paper we examine a number of term rewriting system for integer number representations, building further upon the datatype defining systems described in [2]. In particular, we look at automated methods for proving confluence and…

Convergent rewriting systems on algebraic structures give methods to solve decision problems, to prove coherence results, and to compute homological invariants. These methods are based on higher-dimensional extensions of the critical…