The use of Herbrand functions (more popular;y known as Skolemization) plays an important role in classical theorem proving and logic programing. We define a notion of Herbrand functions for the full intuitionistic predicate calculus. The definition is based on the view that the proof-theoretic role of Herbrand functions ( to replace universal quantifiers), is to ensure that eigenvariable conditions on a sequent proof are respected. the propositional impermutabilities that arise in the intutionistic but not the classical sequent calculus motivate a generalization of the classical notion of Herbrand functions. Proof search using generalized Herbrand functions also provides a framework for generalizing logic programming to subsets of intuitionistic logic that are larger than Horn clauses. The search procedure described here has been implemented and observed to work effectively in practice. The generalization of Herbrand functions can also be applied to sequent calculi formalization of logics other than intuitionistic predicate calculus.

• cade92-ns.dvi.gz
• cade92-ns.ps