de Champeaux, Dennis Faster linear unification algorithm. (English) Zbl 1512.68127 J. Autom. Reasoning 66, No. 4, 845-860 (2022). MSC: 68Q42 68V15 PDFBibTeX XMLCite \textit{D. de Champeaux}, J. Autom. Reasoning 66, No. 4, 845--860 (2022; Zbl 1512.68127) Full Text: DOI
Albert, Luc; Casas, Rafael; Fages, François Average-case analysis of unification algorithms. (English) Zbl 0779.68043 Theor. Comput. Sci. 113, No. 1, 3-34 (1993). Reviewer: L.Albert MSC: 68Q25 68N17 68W30 PDFBibTeX XMLCite \textit{L. Albert} et al., Theor. Comput. Sci. 113, No. 1, 3--34 (1993; Zbl 0779.68043) Full Text: DOI
De Champeaux, Dennis About the Paterson-Wegman linear unification algorithm. (English) Zbl 0645.68103 J. Comput. Syst. Sci. 32, 79-90 (1986). MSC: 68T15 68N25 68W99 68Q25 PDFBibTeX XMLCite \textit{D. De Champeaux}, J. Comput. Syst. Sci. 32, 79--90 (1986; Zbl 0645.68103) Full Text: DOI