Logged Rewriting for Monoids

A rewriting system is a set of equations over a given set of terms called rules that characterize a system of computation and is a powerful general method for providing decision procedures of equational theories, based upon the principle of replacing subterms of an expression with other terms. In particular, a string rewriting system is usually associated with a monoid presentation. At the first level the problem is to decide which combinations of the generators are equivalent under the given rules; Knuth-Bendix completion of the string rewriting system is one of the most successful mechanisms for solving this problem. At the second level, the problem involves determining which combinations of rules are equivalent. Logged rewriting is a technique which not only transforms strings but records the transformation in terms of the original system of rules. The relations between combinatorial, homotopical and homological finiteness conditions for monoids prompt us to consider using computer-friendly rewriting systems to calculate homotopical and homological structure from monoid presentations.