Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Farmer's Theorem revisited

Margus Veanes

Abstract

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.

Details

Publication typeArticle
Published inInformation Processing Letters
URLhttp://dx.doi.org/10.1016/S0020-0190(00)00029-6
Pages47-53
Volume74
Number1-2
PublisherElsevier
> Publications > Farmer's Theorem revisited