Higher-order unification and matching (Q2751368)

The author presents a review of unification algorithms for a higher-order unification. It is well known that higher-order logic is just one among several variants of set theory and the choice of this particular variant could only be justified if it was more adequate for automatization than others.NEWLINENEWLINENEWLINEThe author reviews a few formalizations of set theory -- naïve set theory, type theory, Church's type theory, equational higher-order unification. He remarks that fully automated theorem-proving methods have not permitted to solve really difficult mathematical problems. On the other hand, automated theorem proving methods have found other fields where they have provided genuinely useful services (logic programming, deductive data bases, etc). Besides automated theorem-proving, higher-order unification has also been used to design type reconstruction algorithms for some programming languages, in computational linguistics, program transformation, higher-order rewriting, proof theory etc.NEWLINENEWLINENEWLINEThe author shows that higher-order unification is undecidable by reducing Hilbert's tenth problem, but this problem is semi-decidable. Then the author describes Huet's algorithm, which terminates for some subcases of the problem. Besides building a semi-decision algorithm, the author is interested in identifying decidable subcases. He presents a few decidable subcases of higher-order unification. The main conjectures in this area are decidability of pattern-matching and decidability of context unification.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].