Martelli, Alberto; Montanari, Ugo An efficient unification algorithm. (English) Zbl 0478.68093 ACM Trans. Program. Lang. Syst. 4, 258-282 (1982). Page: −5 −4 −3 −2 −1 ±0 +1 +2 +3 +4 +5 Show Scanned Page Cited in 5 ReviewsCited in 144 Documents MathOverflow Questions: On a surprising property of free theories MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 03B10 Classical first-order logic 03F20 Complexity of proofs 03B35 Mechanization of proofs and logical operations Keywords:unification problem; nondeterministic algorithm; complexity of proof procedures; mechanical theorem proving; resolution PDF BibTeX XML Cite \textit{A. Martelli} and \textit{U. Montanari}, ACM Trans. Program. Lang. Syst. 4, 258--282 (1982; Zbl 0478.68093) Full Text: DOI OpenURL