Herbrand constraint abduction

In this paper we explore abduction over the Herbrand domain - equations on the algebra of finite terms (or finite trees) - which is a central element of logic programming and first-order automated reasoning. This paper is a case study of constraint abduction in the Herbrand domain. The direct relationship between Herbrand constraint abduction and type inference outlined above should make it easy to interpret the results of this paper in the context of type inference.