Since the late nineteenth century, various logicians have set down a number of different calculi for the formalization of first-order predicate logic. The purpose of a first-order calculus is to provide a framework for the study of logical inference and the derivation of first-order predicate formulas. In this book, the author examines several of these calculi and addresses the question, Given two calculi, can any derivation (or proof) in one calculus be simulated in the other calculus in polynomial time (a “p-simulation”)? The author uses the term p-simulation to mean that the length of the proof in one calculus, when transformed into another calculus, has polynomial growth. The discussion centers around calculi that are most appropriate for use in automatic theorem proving.

The first chapter briefly describes the resolution calculus, the connection method, the consolution calculus, the tableau calculus, an adaptation of Gentzen’s sequent calculus, the calculus of natural deduction, and the Frege-Hilbert calculus. The chapter includes an elementary discussion of the merits of the calculi and of their use in automatic theorem proving systems. In the second chapter, the author describes a method for transforming a formula in first-order predicate logic into a normal form called the conjunctive normal form or the clausal form. The clausal form is used in the resolution calculus, and it is a useful form for the comparison of two different calculi. Chapter 2 also describes a p-simulation of the connection calculus by the resolution calculus; that is, Eder shows that any proof in the connection calculus can be simulated in the resolution calculus in polynomial time. The author also shows, with counterexamples, that the converse is not true; that is, in general, the resolution calculus cannot p-simulate the connection calculus. In addition, the author shows that a version of the connection method can be p-simulated in the tableau calculus and vice versa. In chapter3 the author generalizes Tseitin’s extension rule (a deduction rule for clausal form formulas in propositional logic) to first-order logic and applies it to the resolution method to create an extended definitional resolution calculus. This new calculus can p-simulate the sequent calculus, the natural deduction calculus, and the Frege-Hilbert calculus. In chapter 4 the author presents a calculus, called the connection structure calculus, that is a generalized resolution calculus with an additional structure on top of it. The author shows that the connection structure calculus can p-simulate the resolution method (which is not true of the standard connection calculus).

Although the discussion portions of this book are written in a clear, informal style, the key elements of the author’s work are embodied in the definitions, propositions, theorems, and proofs; hence, the reader should be familiar with the fundamentals of first-order predicate logic. The book is well organized with a good set of references. This work should be of particular interest to researchers in automatic theorem proving: the author presents some essential material and important concepts and techniques for the analysis, comparison, and evaluation of first-order calculi for automatic theorem proving systems.