In this first chapter the close connection between a natural text and a corresponding formalized statement in first-order logic will be demonstrated with a simple example. It comprises an informal description of well-known rules of inference (modus ponens, contraposition, and instantiation). As a first illustration the corresponding proof with the connection method is presented. Because of its introductory nature this chapter might well be skipped by alert readers. On the other hand, readers who have no background in mathematical logic at all, might feel a need for a broader introduction. They should consult [R0.3], or any elementary introduction to mathematical logic, such as [He1. In [ko3] they would find many more examples of practical interest.
This chapter provides an introduction into propositional logic, mainly under the aspect of ATP. In particular, its formulas are mostly considered as matrices which are sets of sets of ... of literals thus providing a strictly set-theoretical approach to propositional logic.
The expressive power of propositional logic is too restricted for practical use. Therefore we have to encounter the considerably richer language of first-order logic which will be introduced in the first section of the present chapter. We did not waste our time, however, by the previous development of the connection method for sentential logic. Rather we shall see that the method may be lifted from the ground level to the level of first-order logic by adding some features without any change of the features developed thus far.
For one and a half decades the field of ATP has been dominated by resolution. Not mentioning resolution in the first three out of five chapters, as we did in this book, could therefore be misinterpreted as a provocation. The real reason for this kind of treatment, however, is the fact that with the connection method at hand resolution may be explained in an elegant way, which is carried out in the first section of the present chapter. It even turns out in section 2 that a certain linear refinement of resolution differs from the connection method in representational details only. Hence, the contents of the previous chapters is actually not so far from resolution as it might have appeared.
In a well-balanced monograph on ATP the material treated so far in the previous chapters would perhaps amount to 1/10 of the whole volume. In other words we would now have to proceed with another 36 chapters which is obviously impossible. In other words this book is not at all a well-balanced treatise rather it is relatively detailed in topics discussed so far and is short, to say the least, for the rest.
