-
Chapter and Conference Paper
Correctness of Context-Moving Transformations for Term Rewriting Systems
Proofs by induction are often incompatible with functions in tail-recursive form as the accumulator changes in the course of unfolding the definitions. Context-moving and context-splitting (Giesl, 2000) for fu...
-
Chapter and Conference Paper
Automated Proofs of Unique Normal Forms w.r.t. Conversion for Term Rewriting Systems
The notion of normal forms is ubiquitous in various equivalent transformations. Confluence (CR), one of the central properties of term rewriting systems (TRSs), concerns uniqueness of normal forms
-
Chapter and Conference Paper
Confluence and Commutation for Nominal Rewriting Systems with Atom-Variables
Nominal rewriting was introduced as an extension of first-order term rewriting by a binding mechanism based on the nominal approach. Recently, a new format of nominal rewriting has been introduced where rewrit...
-
Chapter and Conference Paper
A Critical Pair Criterion for Level-Commutation of Conditional Term Rewriting Systems
The rewrite relation of a conditional term rewriting system (CTRS) can be divided into a hierarchy of rewrite relations of term rewriting systems (TRSs) by the depth of the recursive use of rewrite relation in...