Please see books/hints/ for books relevant to the paper,
"Automatically Computing Functional Instantiations", by J Moore.