Farmer's Theorem revisited

The main result is that there is an integer n, such that second-order unification is undecidable in all non-monadic second-order term languages with at least n first-order variables, and even if the arguments of all second-order variables are ground terms of size bounded by n and the total number of variable occurrences is at most n.

In  Information Processing Letters

Publisher  Elsevier
Copyright © 2007 Elsevier B.V. All rights reserved.

Details

TypeArticle
URLhttp://dx.doi.org/10.1016/S0020-0190(00)00029-6
Pages47-53
Volume74
Number1-2
> Publications > Farmer's Theorem revisited