4 Advances and Problems in Mechanical Proof Procedures D. Prawitz

The necessary logical apparatus can be kept remarkably simple. We use a formulation of predicate logic containing individual constants and function symbols. To simplify the description of the method, it is convenient to restrict the formulae F to which the method is applicable. Firstly, it is supposed that F is closed and in prenex normal form. Secondly, it is supposed that all existential quantifiers are eliminated. To see how this can The main part of this paper was also presented in lectures at the University of Stockholm and the Technische Hochschule of Hanover in the spring of 1967.