The first-order theory of rewriting is a decidable theory for finite left-linear right-ground rewrite systems, implemented in FORT. We present a formally verified variant of the decision procedure for the class of linear variable-separated rewrite systems. This variant supports a more expressive theory and is based on the concept of anchored ground tree transducers. The correctness of the decision procedure is verified by a formalization in Isabelle/HOL on top of the Isabelle Formalization of Rewriting (IsaFoR).

Abstract The first-order theory of rewriting is a decidable theory for linear variable-separated rewrite systems. The decision procedure is based on tree automata techniques and recently we completed a formalization in the Isabelle proof assistant. In this paper we present a certificate language that enables the output of software tools implementing the decision procedure to be formally verified. To show the feasibility of this approach, we present , a reincarnation of the decision tool with certifiable output, and the formally verified certifier .

It is well known that (ground) confluence is a decidable property of ground term rewrite systems, and that this extends to larger classes. Here we present a formally verified ground confluence checker for linear, variable-separated rewrite systems. To this end, we formalize procedures for ground tree transducers and so-called RRn relations. The ground confluence checker is an important milestone on the way to formalizing the decidability of the first-order theory of ground rewriting for linear, variable-separated rewrite systems. It forms the basis for a formalized confluence checker for left-linear, right-ground systems.

Toyama’s theorem states that the union of two confluent term rewrite systems with disjoint signatures is again confluent. This is a fundamental result in term rewriting, and several proofs appear in the literature. The underlying proof technique has been adapted to prove further results like persistence of confluence (if a many-sorted term rewrite system is confluent, then the underlying unsorted system is confluent) or the preservation of confluence by currying. In this paper we present a formalization of modularity and related results in Isabelle/HOL. The formalization is based on layer systems, which cover modularity, persistence, currying (and more) in a single framework. The persistence result has been integrated into the certifier CeTA and the confluence tool CSI , allowing us to check confluence proofs based on persistent decomposition, of which modularity is a special case.

It is known that the first-order theory of rewriting is decidable for ground term rewrite systems, but the general technique uses tree automata and often takes exponential time. For many properties, including confluence (CR), uniqueness of normal forms with respect to reductions (UNR) and with respect to conversions (UNC), polynomial time decision procedures are known for ground term rewrite systems. However, this is not the case for the normal form property (NFP). In this work, we present a cubic time algorithm for NFP, an almost cubic time algorithm for UNR, and an almost linear time algorithm for UNC, improving previous bounds. We also present a cubic time algorithm for CR.

Regular tree languages are a popular device for reachability analysis over term rewrite systems, with many applications like analysis of cryptographic protocols, or confluence and termination analysis. At the heart of this approach lies tree automata completion, first introduced by Genet for left-linear rewrite systems. Korp and Middeldorp introduced so-called quasi-deterministic automata to extend the technique to non-left-linear systems. In this paper, we introduce the simpler notion of state-compatible automata, which are slightly more general than quasi-deterministic, compatible automata. This notion also allows us to decide whether a regular tree language is closed under rewriting, a problem which was not known to be decidable before. The improved precision has a positive impact in applications which are based on reachability analysis, namely termination and confluence analysis. Our results have been formalized in the theorem prover Isabelle/HOL. This allows to certify automatically generated proofs that are using tree automata techniques.

The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.

We describe how to utilize redundant rewrite rules, i.e., rules that can be simulated by other rules, when (dis)proving confluence of term rewrite systems. We demonstrate how automatic confluence provers benefit from the addition as well as the removal of redundant rules. Due to their simplicity, our transformations were easy to formalize in a proof assistant and are thus amenable to certification. Experimental results show the surprising gain in power.

This article is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allow to lexicographically combine labelings to show local diagrams decreasing. This approach has two immediate benefits. First, it allows to use labelings for linear rewrite systems also for left-linear ones, provided some mild conditions are satisfied. Second, it admits an incremental method for proving confluence which subsumes recent developments in automating decreasing diagrams. The techniques proposed in the article have been implemented and experimental results demonstrate how, e.g., the rule labeling benefits from our contributions.

We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers. We establish structural conditions on those systems that imply confluence. Our abstract framework covers known results like modularity, many-sorted persistence, layer-preservation, and currying. We present a counterexample to an extension of persistence to order-sorted rewriting and derive new sufficient conditions for the extension to hold. All our proofs are constructive.

We present and compare some well-founded proof orders for decreasing diagrams. These proof orders order a conversion above another conversion if the latter is obtained by filling any peak in the former by a (locally) decreasing diagram. Therefore each such proof order entails the decreasing diagrams technique for proving confluence. The proof orders differ with respect to monotonicity and complexity. Our results are developed in the setting of involutive monoids. We extend these results to obtain a decreasing diagrams technique for confluence modulo.

It is well known that the confluence property of ground term rewrite systems (ground TRSs) is decidable in polynomial time. For an efficient implementation, the degree of this polynomial is of great interest. The best complexity bound in the literature is given by Comon, Godoy and Nieuwenhuis (2001), who describe an O(n^5) algorithm, where n is the size of the ground TRS. In this paper we improve this bound to O(n^3). The algorithm has been implemented in the confluence tool CSI.

We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers. We establish structural conditions on those systems that imply confluence. Our abstract framework covers known results like many-sorted persistence, layer-preservation and currying. We present a counterexample to an extension of the former to order-sorted rewriting and derive new sufficient conditions for the extension to hold.

This paper is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allow to lexicographically combine labelings to show local diagrams decreasing. This approach has two immediate benefits. First, it allows to use labelings for linear rewrite systems also for left-linear ones, provided some mild conditions are satisfied. Second, it admits an incremental method for proving confluence which subsumes recent developments in automating decreasing diagrams. The techniques proposed in the paper have been implemented and experimental results demonstrate how, e.g., the rule labeling benefits from our contributions.