Ideas on dealing with quantifiers

[suhr]

auto procedures in Coq and Agda use a Prolog-like search, which does not deal with quantifiers. But there exists a more general procedure, which allows to solve goals with quantifiers: A proof procedure for the logic of hereditary Harrop formulas

This proof procedure is a basis for several logic programming languages (λProlog, ELPI, Makam), so it might work well in practice.

For higher order formulas you need higher order unification, which is in general undecidable. Fortunately, pattern unification is decidable, and is actually useful in practice.

There are some relevant papers:

• https://arxiv.org/abs/0911.5203
• http://www.lix.polytechnique.fr/~dale/papers/jlc91.pdf
• https://www21.in.tum.de/~nipkow/pubs/lics93.html

UPDATE: also, this paper about Isabelle/HOL might contain relevant references: https://arxiv.org/abs/1907.02836