Essential unifiers

Baader, 1986, Unification in idempotent semigroups is of type zero, J. Automated Reasoning, 2, 10.1007/BF02328451 Baader, 1994, Unification theory Baader, 2001, Unification theory Bürckert, 1989, On equational theories, unification and (un)decidability, J. Symbolic Comput., 8, 3, 10.1016/S0747-7171(89)80021-5 Dershowitz, 1990, Rewrite systems, 244 Eder, 1985, Properties of substitutions and unifications, J. Symbolic Comput., 1, 31, 10.1016/S0747-7171(85)80027-4 Huet, 1981, A complete proof of correctness of the Knuth and Bendix completion algorithm, J. Comput. System Sci., 23, 11, 10.1016/0022-0000(81)90002-7 Kirchner Plotkin, 1972, Building-in equational theories, Machine Intelligence, 7, 73 Robinson, 1965, A machine-oriented logic based on the resolution principle, J. ACM, 12, 23, 10.1145/321250.321253 Schmidt-Schauß, 1986, Unification under associativity and idempotence is of type nullary, J. Automated Reasoning, 2, 10.1007/BF02328450 J. Siekmann, Unification and matching problems, Ph.D. thesis, Essex University, 1975 Siekmann, 1982, A noetherian and confluent rewrite system for idempotent semigroups, Semigroup Forum, 25, 83, 10.1007/BF02573590 Siekmann, 1989, Unification theory, J. Symbolic Comput., 7, 207, 10.1016/S0747-7171(89)80012-4 P. Szabó, Unifikationstheorie erster Ordnung, Ph.D. thesis, University Karlsruhe, 1982 Varzi, 1996, Parts, wholes, and part-whole relations, The prospects of mereotopology, Data and Knowledge Engineering (DKE) J., 20