Undecidability of the Horn-clause implication problem

The authors prove that the problem `given two Horn clauses ℋ ₁=(α₁∧α₂→β) and ℋ₂=(γ₁∧ . . . ∧γ_k→δ), where α_i, β, γ_i, δ are atomic formulas, decide if ℋ₂, is a consequence of ℋ₁´ is not recursive. This solves one of the last open decidability problems concerning formulas in pure predicate logic (i.e. without equality symbol). The proof depends on a thorough analysis of derivation trees of one rule of inference with two premisses and one conclusion, and it may have further applications