4
$\begingroup$

There is concept of Term Rewriting. If one have rules for rewriting terms, one can obtain some term from another. For example, rule1: a -> f(b); rule2: b->t. Term A(f(t)) can be obtained from term A(a) by rule1 and rule2. Terms A(f(t)) and A(a) are congruent terms.

Are there algorithms, which can answer is some term T1 can be obtained from some term T2, by some rules. In other words, whether the two terms are congruent?

I'm also interested in terms with variables.

3 Answers 3