Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
One may consult in this matter e.g. papers collected in the monographic volume of Studia Logica (1998) devoted to automated ND.
- 2.
- 3.
Von Plato discovered that Gentzen himself has proved a normalization theorem for intuitionistic ND; he published Gentzen’s version in [213].
- 4.
- 5.
The exception for classical logic is the work of Sieg mentioned above.
- 6.
In fact, only special sort of such analytic applications is needed. For details see Section 3.3.
- 7.
For those who prefer TS with rules introducing parameters instead of free variables the system KMP may be more convenient.
- 8.
The same result may be demonstrated by showing that any β may be used to creation of new subderivations at most \(2^{n+1}\) times, where n is the number of β-formulae preceding this \(\beta \) in the derivation.
- 9.
Such a solution was applied by the author in [147].
- 10.
As we will see in Chapter 10 the application of cut in modal logics may lead to other problems, as well.
- 11.
This is somewhat related to the strategies from resolution provers, like ordering or selection function, which are applied to reduce the number of useless inferences. But it is not possible to transfer these strategies directly to ordinary ND since it does not work on clauses – one more good reason to introduce RND in the next section.
- 12.
But remember that these results should not be treated as indicating the weakness of tableaux for automated deduction in general, since the possibility of obtaining shorter proofs does not mean that the space of proof search is also smaller; sometimes it is just the opposite. We have mentioned about that already in Chapter 3.
- 13.
One may find it also in [150].
Reference
Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.
Bolotov, A., V. Bocharov, A. Gorchakov, and V. Shangin. 2005. Automated first order natural deduction. In Proceedings of IICAI, 1292–1311.
Smullyan, R. 1968. First-order logic. Berlin: Springer.
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.
Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.
Pollock, J.L. Natural deduction. Available on http://oscarhomme.soc-sci.arizona.edu/ftp/publications.html
Aho, A.V., and J.D. Ullman. 1995. Foundations of computer science. New York: W.H. Freeman and CO.
Cellucci, C. 1992. Existential instatiation and normalization in sequent natural deduction. Annals of Pure and Applied Logic 58: 111–148.
Pelletier, F.J. 1998. Automated natural deduction in THINKER. Studia Logica 60: 3–43.
Chang, C.L., and R.C.T. Lee. 1973. Symbolic logic and mechanical theorem proving. Orlando: Academic Press.
Borićić, B.R. 1985. On sequence-conclusion natural deduction systems. Journal of Philosophical Logic 14: 359–377.
Davis, M., and H. Putnam. 1960. A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7: 201–215.
Pollock, J.L. 1992. Interest driven suppositional reasoning. Journal of Automated Reasoning 6: 419–462.
Indrzejczak, A. 2002. Resolution based natural deduction. Bulletin of the Section of Logic 31(3): 159–170.
Portoraro, D.F. 1998. Strategic construction of Fitch-style proofs. Studia Logica 60: 45–67.
Quine W. Van O. 1950. Methods of logic. New York: Colt.
Sieg, W., and J. Byrnes. 1998. Normal natural deduction proofs (in classical logic). Studia Logica 60: 67–106.
Seldin, J. 1989. Normalization and excluded middle I. Studia Logica, 48: 193–217.
Plato von, J. 2008. Gentzen’s prof of normalization for ND. The bulletin of symbolic logic 14(2): 240–257.
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.
Negri, S., and J. von Plato. 2001. Structural proof theory, Cambridge: Cambridge University Press.
Prawitz, D. 1965. Natural deduction. Stockholm: Almqvist and Wiksell.
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.
Stalmarck, G. 1991. Normalizations theorems for full first order classical natural deduction. The Journal of Symbolic Logic 56: 129–149.
Smullyan, R. 1965. Analytic natural deduction. The Journal of Symbolic Logic 30(2): 123–139.
Troelstra, A.S., and H. Schwichtenberg. 1996. Basic proof theory. Oxford: Oxford University Press.
Indrzejczak, A. 2001. Decision procedure for modal logics in natural deduction setting. Unpublished version, Łódź.
Loveland, D.W. 1978. Automated theorem proving: A logical basis. Amsterdam: North Holland.
Restall, G. Proof theory and philosophy. Available on http://consequently.org/writing/ptp
Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.
Smullyan, R. 1966. Trees and nest structures. The Journal of Symbolic Logic 31(3): 303–321.
Raggio, A. 1965. Gentzen’s hauptsatz for the systems NI and NK. Logique et Analyse 8: 91–100.
Areces, C., H. DeNivelle, and M. DeRijke. 2001. Resolution in modal, description and hybrid logic. Journal of Logic and Computation 11: 717–736.
Kalish, D., and R. Montague. 1964. Logic, techniques of formal reasoning. New York: Harcourt, Brace and World.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2010 Springer Science+Business Media B.V.
About this chapter
Cite this chapter
Indrzejczak, A. (2010). Extended Natural Deduction. In: Natural Deduction, Hybrid Systems and Modal Logics. Trends in Logic, vol 30. Springer, Dordrecht. https://doi.org/10.1007/978-90-481-8785-0_4
Download citation
DOI: https://doi.org/10.1007/978-90-481-8785-0_4
Published:
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-8784-3
Online ISBN: 978-90-481-8785-0
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)