Skip to main content
SpringerLink
Log in
Book cover

Natural Deduction, Hybrid Systems and Modal Logics pp 75–94Cite as

Other Deductive Systems

  • Chapter
  • First Online:

  • 992 Accesses

Part of the book series: Trends in Logic ((TREN,volume 30))

Abstract

The Chapter provides a set of preliminary notes to the next one, where several forms of extended ND systems are discussed. These nonstandard forms of ND are strongly based on solutions occuring in different kinds of deductive systems. Therefore we need to recall some basic information concerning them, which is taken up successively in two sections: the first presents sequent and tableau calculi, systems strongly connected with ND; the second deals with systems popular in automated theorem proving like resolution and Davis/Putnam procedure. It happens that the latter systems are based on the application of cut, whereas the former rather tend to eliminate this rule in practice.

It should be noted that the presentation of different types of deductive systems has an elementary character and is limited in two senses. From the variety of systems we have selected only those that are used further as the source of inspiration in building the enriched versions of ND, particularly in the setting of formalization of modal logic. In result many important kinds of deductive systems like connection calculi, goal oriented proof systems or refutation calculi, are not taken into account. Either we do not know how to take advantage of them for the needs of ND (which is not to say that it is not possible!), or they were not used in modal logic, at least not in the way suitable for our purposes. Moreover, we focus only on some theoretical aspects of the discussed systems that are vital for us. In particular, we focus upon the cut rule and its importance for strategies of proof search, and to some related properties of rules like: subformula property, analyticity, confluency.

The last section of this Chapter contains a discussion of some complexity problems connected with cut and its elimination or bounded application. Again, because of the rudimentary character, much of this Chapter may be skipped in the first reading and consulted when necessary in further lecture.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   189.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   249.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   249.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    In fact, the original system of Gentzen is defined on sequents formed from finite lists of formulae, however this is not of importance here.

  2. 2.

    Poggiolesi [214] contains an interesting historical exposition of this concept.

  3. 3.

    Cf. Display Calculus [280], or SC of Mints [190] for S5.

  4. 4.

    In fact, both authors prefer metalinguistic devices: Lis uses + for assertion and – instead of negation, Smullyan uses prefixes T and F.

  5. 5.

    In what follows we will sometimes use the same name for different variants of essentially the same rule in related systems if it does not cause misunderstanding.

  6. 6.

    E.g. a classic Chang and Lee [68]; particularly usefull presentations for our purposes are Gallier [101] and Fitting [95].

  7. 7.

    Clearly, this success was not only the result of simplicity of the original approach but also of the development of several optimization techniques and refinements of original system. One may mention here the introduction of hiperresolution, linear resolution, ordering of literals, selection function e.t.c.

  8. 8.

    One can find a useful survey in [84],[10].

  9. 9.

    In standard procedures of transformation it may lead to the exponential blow up, but at present much better techniques are applied, cf. e.g. [196],242]) for methods of structure-preserving reduction working in polynomial time.

  10. 10.

    In fact, all DP rules are also used as simplification strategies in resolution or tableau-based provers.

  11. 11.

    In fact, modern tableau-based provers often work on clauses which simplifies adaptation of strategies developed in the setting of resolution.

  12. 12.

    Note that this simplification applies to the formalization of classical logics; it is not necessarily true on the ground of nonclassical logics, where many proposed SC’s and TS’s are not in such direct relationship. In case of modal logics cf. Chapter 7 for details.

  13. 13.

    It was Boolos who for the first time paid an attention to this problem, see [51] and a detailed discussion in D’Agostino [2] and Fitting [95].

  14. 14.

    For example, the use of lemmata or merging, cf. [02].

  15. 15.

    For more about it cf. e.g. Hähnle [120] and especially a study of Plaisted and Zhu [211]), where formal treatment of proof search space is provided for many types of calculi.

Reference

  1. Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.

    Google Scholar 

  2. Mints, G. 1970. Cut-free calculi of the S5 type. Studies in Constructive Mathematics and Mathematical Logic II: 79–82.

    Google Scholar 

  3. Schmidt, R.A., and U. Hustadt. First-order methods for modal logics. Volume in memoriam of Harold Ganzinger, Lecture Notes in AI, Appear in eds. A. Podelski, A. Voronkov, and R. Wilhelm. Springer.

    Google Scholar 

  4. Prawitz, H., D. Prawitz, and N. Voghera. 1960. A mechanical proof procedure and its realization in an electronic computer. Journal of the Association for Computing Machinery 7: 102–128.

    Google Scholar 

  5. Smullyan, R. 1968. First-order logic. Berlin: Springer.

    Google Scholar 

  6. Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.

    Google Scholar 

  7. Beth, E. 1955. Semantic entailment and formal derivability. Mededelingen der Kon. Ned. Akad. v. Wet. 18(13).

    Google Scholar 

  8. Schütte, K. 1977. Proof theory. Berlin: Springer.

    Google Scholar 

  9. Stachniak, Z., and P. O’Hearn. 1990. Resolution in the domain of strongly finite logics. Fundamenta Informaticae 13: 333–351.

    Google Scholar 

  10. Chang, C.L., and R.C.T. Lee. 1973. Symbolic logic and mechanical theorem proving. Orlando: Academic Press.

    Google Scholar 

  11. Poggiolesi, F. 2008. Sequent calculi for modal logics, Ph.D Thesis, Florence.

    Google Scholar 

  12. 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. Boolos, G. 1984. Don’t eliminate cut. Journal of Philosophical Logic 7: 373–378.

    Google Scholar 

  14. Rasiowa, H., and R. Sikorski. 1963. The mathematics of metamathematics. Warszawa: PWN.

    Google Scholar 

  15. Schmidt, R.A. 2006. Developing modal tableaux and resolution methods via first-order resolution. In Advances in modal logic 6, ed. M. deRijke, 107–135. Dordrecht: Kluwer.

    Google Scholar 

  16. Wang, H. 1960. Toward mechanical mathematics. IBM Journal of Research and Development 4: 2–22.

    Article  Google Scholar 

  17. Plaisted, D.A., and Y. Zhu. 1997. The efficiency of theorem proving strategies: A comparative and assymptotic analysis. Braunschweig: Vieweg Verlag.

    Google Scholar 

  18. De Nivelle, H., R.A. Schmidt, and U. Hustadt. 2000. Resolution-based methods for modal logics. Logic Journal of the IGPL 8(3): 265–292.

    Article  Google Scholar 

  19. Gallier, J.H. 1986. Logic for computer science. New York: Harper and Row.

    Google Scholar 

  20. Kleene, S.C. 1952. Introduction to metamathematics. Amsterdam: North Holland.

    Google Scholar 

  21. Hustadt, U., and R.A. Schmidt. 2002. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning 28(2): 205–232.

    Article  Google Scholar 

  22. Wansing, H. 1998. Displaying modal logics. Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  23. 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. Gentzen, G. 1934. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift 39: 176–210, 405–431.

    Article  Google Scholar 

  25. Hähnle, R. 2001. Tableaux and related methods. In Handbook of automated reasoning, eds. A. Robinson, and A. Voronkov, pp. 101–177. Amsterdam: Elsevier.

    Google Scholar 

  26. Takano, M. 1992. Subformula property as a substitute for cut-elimination in modal propositional logics. Mathematica Japonica 37(6): 1129–1145.

    Google Scholar 

  27. Farinas del Cerro, L., and A. Herzig. 1995. Modal deduction with applications in epistemic and temporal logics. In Handbook of logic in artificial intelligence and logic programming, eds. D. Gabbay et al., vol IV, 499–594. Oxford: Clarendon Press.

    Google Scholar 

  28. Hustadt, U., and R.A. Schmidt. 2000. Issues of decidability for description logics in the framework of resolution. In Automated deduction in classical and non-classical logics, eds. R. Caferra, and G. Salzer, 192–206. New York: Springer.

    Google Scholar 

  29. Loveland, D.W. 1978. Automated theorem proving: A logical basis. Amsterdam: North Holland.

    Google Scholar 

  30. Avron, A. 1993. Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning 10(2): 265–281.

    Article  Google Scholar 

  31. Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.

    Article  Google Scholar 

  32. Lis, Z. 1960. Wynikanie semantyczne a wynikanie formalne. Studia Logica 10: 39–60.

    Article  Google Scholar 

  33. Orłowska, E. 1987. Relational interpretation of modal logics. Technical Report ICSPas.

    Google Scholar 

  34. Priest, G. 2001. An introduction to non-classical logic. Cambridge: Cambridge University Press.

    Google Scholar 

  35. D’Agostino, M. et al. (eds.). 1999. Handbook of tableau methods. Dordrecht: Kluwer Academic Publishers.

    Google Scholar 

  36. Hintikka, J. 1955. Form and content in quantification theory. Acta Philosophica Fennica 8: 8–55.

    Google Scholar 

  37. Areces, C., H. DeNivelle, and M. DeRijke. 2001. Resolution in modal, description and hybrid logic. Journal of Logic and Computation 11: 717–736.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. Logic, University of Lódz, Kopcinskiego 16/18, 90-232, Lódz, Poland

    Dr. Andrzej Indrzejczak

Authors
  1. Dr. Andrzej Indrzejczak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrzej Indrzejczak .

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Indrzejczak, A. (2010). Other Deductive Systems. 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_3

Download citation

Publish with us

Policies and ethics

Search

Navigation