Ground confluence of term rewriting systems guarantees that all ground terms are confluent.
Recently, interests in proving confluence of term rewriting systems automatically has grown …

Automated inductive reasoning for term rewriting has been extensively studied in the
literature. Classes of equations and term rewriting systems (TRSs) with decidable inductive …

In many automated methods for proving inductive theorems, finding a suitable
generalization of a conjecture is a key for the success of proof attempts. On the other hand …

Recently, rewriting induction, which is one of the induction principles for proving inductive
theorems in equational theory, has been extended to deal with constrained term rewriting …

Term rewrite systems have been extensively used in order to model computer programs for
the purpose of formal verification. This is in particular true if the termination behavior of …

Higher-order rewriting systems (HRSs) is a formalism of rewriting with variable binding and
higher-order functions [2]. Higher-order rewriting deals with simply-typed lambda-terms with …

We present an automated lemma generation method for equational, inductive theorem
proving based on the term rewriting induction of Reddy and Aoto as well as the divergence …

Equations are a versatile and natural tool for various reasoning tasks. This thesis
investigates how to fully automate equational reasoning. Central to automation is Knuth and …

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 …

AGCP (Automated Groud Confluence Prover)[1] is a tool for proving ground confluence of
many-sorted term rewriting systems. AGCP is written in Standard ML of New Jersey …