# SMT solves with functions for free varibles

So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions which are counter examples to predicates (or solutions to the inverse rather). I would like to restrict the functions to some small class however (possibly even smaller than primitive recursive) so I think there is hope of this working if I restrict them enough.

Has any work been done in this area? Have any tools been written for such things?

• What kind of predicates? For some kinds what you propose is trivial, for many others it's undecidable. – Raphael Dec 8 '14 at 20:00
• The Keyword you are looking for is Higher-Order Unification. See also here. – cody Dec 8 '14 at 20:34
• Perhaps I just don't see the trivial way to use Higher-Order Unification as a means to find solutions to this. For instance $len (xs ++ ys) = (len xs) + (len ys)$. This is clearly easy to find a counter example to (constant 1 function) but I don't see how higher order unification helps me with that. – Jake Dec 9 '14 at 0:19
• $\newcommand\doubleplus{+\kern-1.3ex+\kern0.8ex}$ looks like the latex came out really bad this looks better: $len(xs \doubleplus ys) = len\,\,xs + len\,\,ys$ – Jake Dec 9 '14 at 2:21