# Quantum algorithms for the first-order and higher-order unification problem (finding substitution)

Unification https://en.wikipedia.org/wiki/Unification_(computer_science) is the most important algorithm for symbolic computation and automatic theorem proving - essentially - it allows to find the candidate formulas that can be used for performing the next steps of inference (be it resolution in the backward chaining or other algorithms in the forward chaining). My question is - are the quantum algorithms for the unification? Google gives nothing, but I guess that there are algorithms and some perspective but different terms are used and Google can not match such research.