A subset of λProlog, called Lλ, was presented in [Mil91] where it was shown that an implementation of proof search could be written in which only a small subset of higher-order unification was required. Furthermore, that subset was decidable, unary, and did not need typing information. This subset of unification was called Lλ-unification in [Mil91] but is now more commonly referred to as higher-order pattern unification [Nip93, NL05]. In that subset, variables in functional position are applied to distinct variables which must be bound in the scope of the binding of the functional variable.
exists X, forall y z, X y z = y
can be solved, but
exists X, forall y, X y y = y
can’t, as it violates the first constraint (so that
take at least two values,
x1\ x2\ x1 and
x1\ x2\ x2), and
forall y, exists X, forall z, X y z = y
can’t either, as it violates the second constraint and therefore could be rewritten
exists X', forall y z, (X' y) y z = y
Bedwyr uses an extension of this higher-order pattern unification which handles ∇.