Extended Natural Deduction

  • Andrzej IndrzejczakEmail author
Part of the Trends in Logic book series (TREN, volume 30)


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.


Modal Logic Inference Rule Consistency Test Proof Assistant Elimination Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [95]
    Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.Google Scholar
  2. [46]
    Bolotov, A., V. Bocharov, A. Gorchakov, and V. Shangin. 2005. Automated first order natural deduction. In Proceedings of IICAI, 1292–1311.Google Scholar
  3. [261]
    Smullyan, R. 1968. First-order logic. Berlin: Springer.Google Scholar
  4. [117]
    Goré, R. 1999. Tableau methods for modal and temporal logics. In Handbook of tableau methods, eds. M. D’Agostino et al., 297–396. Dordrecht: Kluwer Academic Publishers.Google Scholar
  5. [93]
    Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.Google Scholar
  6. [217]
    Pollock, J.L. Natural deduction. Available on
  7. [3]
    Aho, A.V., and J.D. Ullman. 1995. Foundations of computer science. New York: W.H. Freeman and CO.Google Scholar
  8. [65]
    Cellucci, C. 1992. Existential instatiation and normalization in sequent natural deduction. Annals of Pure and Applied Logic 58: 111–148.CrossRefGoogle Scholar
  9. [204]
    Pelletier, F.J. 1998. Automated natural deduction in THINKER. Studia Logica 60: 3–43.CrossRefGoogle Scholar
  10. [68]
    Chang, C.L., and R.C.T. Lee. 1973. Symbolic logic and mechanical theorem proving. Orlando: Academic Press.Google Scholar
  11. [53]
    Borićić, B.R. 1985. On sequence-conclusion natural deduction systems. Journal of Philosophical Logic 14: 359–377.CrossRefGoogle Scholar
  12. [77]
    Davis, M., and H. Putnam. 1960. A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7: 201–215.Google Scholar
  13. [216]
    Pollock, J.L. 1992. Interest driven suppositional reasoning. Journal of Automated Reasoning 6: 419–462.Google Scholar
  14. [150]
    Indrzejczak, A. 2002. Resolution based natural deduction. Bulletin of the Section of Logic 31(3): 159–170.Google Scholar
  15. [219]
    Portoraro, D.F. 1998. Strategic construction of Fitch-style proofs. Studia Logica 60: 45–67.CrossRefGoogle Scholar
  16. [226]
    Quine W. Van O. 1950. Methods of logic. New York: Colt.Google Scholar
  17. [254]
    Sieg, W., and J. Byrnes. 1998. Normal natural deduction proofs (in classical logic). Studia Logica 60: 67–106.CrossRefGoogle Scholar
  18. [247]
    Seldin, J. 1989. Normalization and excluded middle I. Studia Logica, 48: 193–217.CrossRefGoogle Scholar
  19. [213]
    Plato von, J. 2008. Gentzen’s prof of normalization for ND. The bulletin of symbolic logic 14(2): 240–257.CrossRefGoogle Scholar
  20. [81]
    Dyckhoff, R. 1987. Implementing a simple proof assistant. In Proceedings of workshop on programming for logic teaching, eds. J. Derrick, and H.A. Lewis, 49–59.Google Scholar
  21. [193]
    Negri, S., and J. von Plato. 2001. Structural proof theory, Cambridge: Cambridge University Press.Google Scholar
  22. [220]
    Prawitz, D. 1965. Natural deduction. Stockholm: Almqvist and Wiksell.Google Scholar
  23. [2]
    D’Agostino, M. 1999. Tableau methods for classical propositional logic. In Handbook of tableau methods, eds. M. D’Agostino et al., 45–123. Dordrecht: Kluwer Academic Publishers.Google Scholar
  24. [263]
    Stalmarck, G. 1991. Normalizations theorems for full first order classical natural deduction. The Journal of Symbolic Logic 56: 129–149.CrossRefGoogle Scholar
  25. [259]
    Smullyan, R. 1965. Analytic natural deduction. The Journal of Symbolic Logic 30(2): 123–139.CrossRefGoogle Scholar
  26. [276]
    Troelstra, A.S., and H. Schwichtenberg. 1996. Basic proof theory. Oxford: Oxford University Press.Google Scholar
  27. [147]
    Indrzejczak, A. 2001. Decision procedure for modal logics in natural deduction setting. Unpublished version, Łódź.Google Scholar
  28. [179]
    Loveland, D.W. 1978. Automated theorem proving: A logical basis. Amsterdam: North Holland.Google Scholar
  29. [232]
    Restall, G. Proof theory and philosophy. Available on
  30. [94]
    Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.CrossRefGoogle Scholar
  31. [260]
    Smullyan, R. 1966. Trees and nest structures. The Journal of Symbolic Logic 31(3): 303–321.CrossRefGoogle Scholar
  32. [227]
    Raggio, A. 1965. Gentzen’s hauptsatz for the systems NI and NK. Logique et Analyse 8: 91–100.Google Scholar
  33. [10]
    Areces, C., H. DeNivelle, and M. DeRijke. 2001. Resolution in modal, description and hybrid logic. Journal of Logic and Computation 11: 717–736.CrossRefGoogle Scholar
  34. [159]
    Kalish, D., and R. Montague. 1964. Logic, techniques of formal reasoning. New York: Harcourt, Brace and World.Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Dept. LogicUniversity of LódzLódzPoland

Personalised recommendations