6 Decidable Subcases
As usual when a problem is undecidable, besides building a semi-decision algorithm, we are also interested in identifying decidable subcases. In this section, we present a few decidable subcases of higher-order unification. These subcases are obtained by restricting the order, the arity or the number of occurrences of variables, or by taking terms of a special form. For some subcases, Huet's algorithm terminates, for others it does not and we must design another algorithm to prove decidability.
The main conjectures in this area are the decidability of pattern-matching, i.e. the subcase of unification where variables occur only in a single side of equations and the decidability of context unification.
6.1 First-order ...
Get Handbook of Automated Reasoning now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.