Abstract. First-order theorem provers are commonly utilised as backends to
proof assistants. In order to improve efficiency, it is desirable that such provers
can carry out some higher-order reasoning. In his 1991 paper, Dougherty pro-
posed a combinatory unification algorithm for higher-order logic. The algorithm
removes the need to deal with λ-binders and α-renaming, making it attractive to
implement in first-order provers. However, since publication it has garnered little
interest due to a number of characteristics that make it unsuitable for a practi-
cal implementation. It fails to terminate on many trivial instances and requires
polymorphism. We present a restricted version of Dougherty’s algorithm that is
incomplete, terminating and does not require polymorphism. Further, we describe
its implementation in the Vampire theorem prover, including a novel use of a sub-
stitution tree as a filtering index for higher-order unification. Finally, we analyse
the performance of the algorithm on two benchmark sets and show that it is com-
petitive