zbMATH — the first resource for mathematics

Incremental construction of unification algorithms in equational theories. (English) Zbl 0516.68067
Automata, languages and programming, 10th Colloq., Barcelona/Spain 1983, Lect. Notes Comput. Sci. 154, 361-373 (1983).

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
08A50 Word problems (aspects of algebraic structures)
03B35 Mechanization of proofs and logical operations
03E20 Other classical set theory (including functions, relations, and set algebra)