ABSTRACT. Process graphs that are interpretations of `1-free' regular expressions in Milner's process semantics for regular expressions have the Loop Existence and Elimination Property (LEE). Hereby a process graph satisfies LEE if the procedure of loop elimination, in which in every step a loop subgraph is decoupled by removing its entry transitions and then garbage collection is performed, terminates in a process graph without an infinite trace. Loop elimination on finite process graphs is a terminating, but typically not confluent. We explain that loop elimination can be turned into a confluent rewrite system on all process graphs by adding pruning steps that remove transitions to deadlocking states. For this purpose we perform a critical-pair like analysis that involves bi-loop subgraphs, and use the decreasing diagram method. This confluence result has two expedient consequences: for finite process graphs, LEE can be decided in polynomial time, and a layered version of LEE (no loops are eliminated from bodies of already eliminated ones) coincides with LEE.

ABSTRACT. Okui proved that simultaneous critical pairs (SCPs) can be used as a sufficient criterion to ensure confluence of term rewrite systems. His definitions, lemmas and proofs where reformulated by Kirk and Middeldorp. They heavily utilize proof terms and finally arrive at a formalized proof of Okui's result in Isabelle/HOL. However, Kirk and Middeldorp's formalization lacks an executable algorithm to compute the set of proof term based SCPs in a verified way. In this work, we provide such an algorithm, and we further modify the formalization in such a way, that SCPs can also be used to show commutation, generalizing the confluence result. Our results have fully been integrated in the certifier CeTA, that now can deal with both commutation- and confluence-proofs by SCPs.

ABSTRACT. We generalize the confluence result for orthogonal higher-order pattern rewrite systems to higher-order rewrite systems whose left hand sides consist of Yokoyama et al.'s deterministic higher-order patterns.

ABSTRACT. We show that for the (untyped) bang-calculus β! is confluent modulo σ.

ABSTRACT. We describe a machine-checked proof of a result in Isabelle/HOL that implies that if the cardinality of a confluent abstract rewriting system (ARS) is below the first uncountable limit cardinal, then confluence of this ARS can be proved with the help of the decreasing diagrams method using 3 labels and such an ARS has a so-called almost deterministic Church-Rosser strategy (defined by weakening conditions of the definition of deterministic one-step Church-Rosser strategies). We also discuss consequences of this result. One consequence is that there is a statement that can be used as additional axiom to HOL that implies that every confluent ARS has an almost deterministic Church-Rosser strategy and that the decreasing diagrams method with 3 labels is complete without cardinality restrictions.

ABSTRACT. Reachability is a central question in term rewriting: can a given target term (e.g., an error state) be reached from a start term? It is also an important property in confluence analysis, and corresponding tools compete in the annual confluence competition. An interesting generalization of this problem is handling programs that can make random choices during execution. For such probabilistic programs, reachability becomes a quantitative property instead of a qualitative one: instead of asking whether the target is reachable, one asks with which probability it is reached. We lift reachability analysis from ordinary term rewriting to probabilistic term rewrite systems. To do so, we formalize the maximal probability of reaching a target term and adapt two techniques for analyzing reachability (based on symbol transition graphs and on term orderings) to compute upper bounds on this probability.

ABSTRACT. In an earlier paper we proved that a transformation due to Snyder generates all canonical TRSs equivalent to a given canonical ground TRS. Here we present an explicit recursive procedure to generate these. We prove its correctness and show how the procedure can be used to obtain the exponential upper bound due to Snyder on the number of canonical ground presentations.

ABSTRACT. Generalized Term Rewriting Systems (GTRSs) extend traditional term rewriting systems by providing a highly expressive framework that integrates conditional rules, context-sensitive constraints, and Horn clauses directly into the rewriting formalism. Recently, we have extended the tools infChecker and MU-TERM to support GTRSs. In this work, we exploit our previous extensions of infChecker and MU-TERM for GTRSs to extend CONFident with corresponding capabilities for proving confluence.

ABSTRACT. We present a stratified normalisation completion procedure for rewriting systems over linear precategories. Our approach relies on a stratification of the set of rewriting rules according to their confluence and termination properties. We introduce stratified termination functions to establish termination for such systems. We illustrate the method on several classes of algebraic structures, including associative and diagrammatic algebras. In these contexts, we show how the stratification of defining rules can be used to compute hom-bases effectively.

ABSTRACT. We describe *completion* procedures to obtain *strongly confluent* TRSs from a set of equations. Strong confluence implies confluence *without requiring termination*. We show the performance of our implementation in TRS.Tool 2 by means of some benchmarks.