On the translation of higher-order problems into first-order logic
Manfred Kerber · 1994
. In most cases higher-order logic is based on the - calculus in order to avoid the infinite set of so-called comprehension axioms. However, there is a price to be paid, namely an undecidable unification algorithm. If we do not use the -calculus, but translate higher-order expressions into firstorder expressions by standard translation techniques, we have to translate the infinite set of comprehension axioms, too. Of course, in general this is not practicable. Therefore such an approach requires some restrictions such as the choice of the necessary axioms by a human user or the restriction to certain problem classes. This paper will show how the infinite class of comprehension axioms can be represented by a finite subclass, so that an automatic translation of finite higher-order problems into finite first-order problems is possible. This translation is sound and complete with respect to a Henkin-style general model semantics. 1 Introduction First-order logic is a powerful tool for ...