4. Extended Natural Deduction

In this Chapter there is a continual emphasis on the application of ND as a tool of proof search and possibly of automation. In particular, we take up the question of how to make ND a universal system. In order to find satisfactory solutions we compare ND with other types of DS’s. Although ND systems are rather rarely considered in the context of automated deduction they presumably accord with each other and ND systems may be turned into useful automatic proof search procedures. Moreover, even if there are some problems with the construction of efficient ND-based provers, it seems that for the widely understood computer-aided forms of teaching logic, ND should be acknowledged. A good evidence for this claim is provided by the increasing number of proof assistants, tutors, checkers and other interactive programs of this sort based on some forms of ND. Section 4.1. is devoted to the general discussion of these questions, whereas the rest of the Chapter takes up successively the presentation of some concrete, universal and analytic versions of ND for classical and free logic.