Calculi for First Order Logic
Elmar Eder · 1992
In this chapter we give a brief description of a few proof calculi for first order predicate logic with function symbols which are suitable for automated theorem proving and most of which have been used in actual implementations by various authors. Section 1.1 gives some basic concepts of first order predicate logic and of automated theorem proving, and some general remarks on the question of the suitability of calculi for the automation of reasoning. The following sections 1.2, 1.3, 1.5, 1.6, 1.7, and 1.8 contain descriptions of resolution, the connection method, the method of tableaux, the sequent calculus, the natural deduction calculus, and a Frege-Hilbert calculus, respectively.