Herbrand procedures
Christopher John Hogger · 1990
Abstract In the early days of automated theorem proving much use was made of the principles discussed in the last Theme: replace the given clause-set by its ground instantiation; then seek a contradiction. The formal justification for this approach relies upon a profound and highly important result in proof theory known as Herbrand’s Theorem. There are many ways of expressing and specializing this theorem, but the specialization of it which follows is perhaps the one best-suited to our present context: