Other Deductive Systems

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


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.


Modal Logic Deductive System Conjunctive Normal Form Sequent Calculus Automate Theorem Prove 
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. [190]
    Mints, G. 1970. Cut-free calculi of the S5 type. Studies in Constructive Mathematics and Mathematical Logic II: 79–82.Google Scholar
  3. [243]
    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. [221]
    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. [261]
    Smullyan, R. 1968. First-order logic. Berlin: Springer.Google Scholar
  6. [93]
    Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.Google Scholar
  7. [27]
    Beth, E. 1955. Semantic entailment and formal derivability. Mededelingen der Kon. Ned. Akad. v. Wet. 18(13).Google Scholar
  8. [244]
    Schütte, K. 1977. Proof theory. Berlin: Springer.Google Scholar
  9. [262]
    Stachniak, Z., and P. O’Hearn. 1990. Resolution in the domain of strongly finite logics. Fundamenta Informaticae 13: 333–351.Google Scholar
  10. [68]
    Chang, C.L., and R.C.T. Lee. 1973. Symbolic logic and mechanical theorem proving. Orlando: Academic Press.Google Scholar
  11. [214]
    Poggiolesi, F. 2008. Sequent calculi for modal logics, Ph.D Thesis, Florence.Google 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. [51]
    Boolos, G. 1984. Don’t eliminate cut. Journal of Philosophical Logic 7: 373–378.Google Scholar
  14. [228]
    Rasiowa, H., and R. Sikorski. 1963. The mathematics of metamathematics. Warszawa: PWN.Google Scholar
  15. [242]
    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. [279]
    Wang, H. 1960. Toward mechanical mathematics. IBM Journal of Research and Development 4: 2–22.CrossRefGoogle Scholar
  17. [211]
    Plaisted, D.A., and Y. Zhu. 1997. The efficiency of theorem proving strategies: A comparative and assymptotic analysis. Braunschweig: Vieweg Verlag.Google Scholar
  18. [196]
    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.CrossRefGoogle Scholar
  19. [101]
    Gallier, J.H. 1986. Logic for computer science. New York: Harper and Row.Google Scholar
  20. [162]
    Kleene, S.C. 1952. Introduction to metamathematics. Amsterdam: North Holland.Google Scholar
  21. [138]
    Hustadt, U., and R.A. Schmidt. 2002. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning 28(2): 205–232.CrossRefGoogle Scholar
  22. [280]
    Wansing, H. 1998. Displaying modal logics. Dordrecht: Kluwer Academic Publishers.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. [109]
    Gentzen, G. 1934. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift 39: 176–210, 405–431.CrossRefGoogle Scholar
  25. [120]
    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. [269]
    Takano, M. 1992. Subformula property as a substitute for cut-elimination in modal propositional logics. Mathematica Japonica 37(6): 1129–1145.Google Scholar
  27. [84]
    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. [137]
    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. [179]
    Loveland, D.W. 1978. Automated theorem proving: A logical basis. Amsterdam: North Holland.Google Scholar
  30. [15]
    Avron, A. 1993. Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning 10(2): 265–281.CrossRefGoogle Scholar
  31. [94]
    Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.CrossRefGoogle Scholar
  32. [178]
    Lis, Z. 1960. Wynikanie semantyczne a wynikanie formalne. Studia Logica 10: 39–60.CrossRefGoogle Scholar
  33. [201]
    Orłowska, E. 1987. Relational interpretation of modal logics. Technical Report ICSPas.Google Scholar
  34. [222]
    Priest, G. 2001. An introduction to non-classical logic. Cambridge: Cambridge University Press.Google Scholar
  35. [121]
    D’Agostino, M. et al. (eds.). 1999. Handbook of tableau methods. Dordrecht: Kluwer Academic Publishers.Google Scholar
  36. [131]
    Hintikka, J. 1955. Form and content in quantification theory. Acta Philosophica Fennica 8: 8–55.Google Scholar
  37. [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

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

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

Personalised recommendations