Higher-order theorem proving (e.g. higher-order resolution) is different from first-order theorem proving in several respects. First, the first-order unification algorithm has to be replaced by the higher-order one. Even then, the resolution rule alone is not complete but another rule called the splitting rule has to be added. At last, the skolemization rule is more complicated.
On the other hand, higher-order logic, also called simple type theory, can be expressed as a first-order theory H, and first-order theorem proving methods, such as first-order resolution, can be used for this theory. Of course, first-order resolution with the axioms H is much less efficient than higher-order resolution. However, we can try to understand higher-order resolution as a special automated theorem proving method designed for the theory H. A motivation for this project is that it is very unlikely that such a method applies only to the theory H, but it should also apply to similar theories such as extensions of type theory with primitive recursion or set theory.
Together with Th. Hardin and C. Kirchner, we have proposed a theorem proving method for first-order logic, called resolution modulo, that when applied to the theory H simulates exactly higher-order resolution. Proving the completeness of this method has required to introduce a new presentation of first-order logic, called deduction modulo that separates clearly computation steps and deduction steps.
Resolution modulo can be applied both to type theory and to set theory. The goal of this talk is to compare how resolution modulo works for one theory and the other. In order to remain self-contained, we will first present shortly the ideas of deduction modulo and of resolution modulo.