# G.Dowek:

Automated Theorem Proving in First-order Logic Modulo:

on the Difference between Set Theory and Simple Type Theory

### Abstract

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.