Jouannaud, Jean-Pierre; Kirchner, Claude; Kirchner, Helene 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). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 19 Documents MSC: 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) Keywords:unification problem; automatic theorem proving; noetherian term rewriting system; equational term rewriting system; incremental way; signed binary trees theory Citations:Zbl 0511.00030 PDFBibTeX XML