Other Deductive Systems

Chapter
Part of the Trends in Logic book series (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.

Keywords

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.

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.
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.
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.
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.
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.
31. 
Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97.
32. 
Lis, Z. 1960. Wynikanie semantyczne a wynikanie formalne. Studia Logica 10: 39–60.
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. 