The unification problem in f'mst-order predicate calculus is described in general terms as the solution of a system of equations, and a nondeterministic algorithm is given. A new unification algorithm, characterized by having the acyclicity test efficiently embedded into it, is derived from the nondeterministic one, and a PASCAL implementation is given. A comparison with other well-known unification algorithms shows that the algorithm described here performs well in all cases.
No takes yet. Share an insight, caveat, or question.
Martelli et al. (1982) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: