This paper introduces a proof procedure that integrates Abductive Logic Programming (ALP) and Inductive Logic Programming (ILP) to automate the learning of first order Horn clause theories from examples and background knowledge. The work builds upon a recent approach called Hybrid Abductive Inductive Learning (HAIL) by showing how language bias can be practically and usefully incorporated into the learning process. A proof procedure for HAIL is proposed that utilises a set of user specified mode declarations to learn hypotheses that satisfy a given language bias. A semantics is presented that accurately characterises the intended hypothesis space and includes the hypotheses derivable by the proof procedure. An implementation is described that combines an extension of the Kakas-Mancarella ALP procedure within an ILP procedure that generalises the Progol system of Muggleton. The explicit integration of abduction and induction is shown to allow the derivation of multiple clause hypotheses in response to a single seed example and to enable the inference of missing type information in a way not previously possible.