Weitere Kapitel dieses Buchs durch Wischen aufrufen
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.
Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten
Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:
Fitting, M. 1996. First-order logic and automated theorem proving. Berlin; Springer.
Mints, G. 1970. Cut-free calculi of the S5 type. Studies in Constructive Mathematics and Mathematical Logic II: 79–82.
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.
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.
Smullyan, R. 1968. First-order logic. Berlin: Springer.
Fitting, M. 1983. Proof methods for modal and intuitionistic logics. Dordrecht; Rei-del.
Beth, E. 1955. Semantic entailment and formal derivability. Mededelingen der Kon. Ned. Akad. v. Wet. 18(13).
Schütte, K. 1977. Proof theory. Berlin: Springer.
Stachniak, Z., and P. O’Hearn. 1990. Resolution in the domain of strongly finite logics. Fundamenta Informaticae 13: 333–351.
Chang, C.L., and R.C.T. Lee. 1973. Symbolic logic and mechanical theorem proving. Orlando: Academic Press.
Poggiolesi, F. 2008. Sequent calculi for modal logics, Ph.D Thesis, Florence.
Davis, M., and H. Putnam. 1960. A computing procedure for quantification theory. Journal of the Association for Computing Machinery 7: 201–215.
Boolos, G. 1984. Don’t eliminate cut. Journal of Philosophical Logic 7: 373–378.
Rasiowa, H., and R. Sikorski. 1963. The mathematics of metamathematics. Warszawa: PWN.
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.
Wang, H. 1960. Toward mechanical mathematics. IBM Journal of Research and Development 4: 2–22. CrossRef
Plaisted, D.A., and Y. Zhu. 1997. The efficiency of theorem proving strategies: A comparative and assymptotic analysis. Braunschweig: Vieweg Verlag.
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. CrossRef
Gallier, J.H. 1986. Logic for computer science. New York: Harper and Row.
Kleene, S.C. 1952. Introduction to metamathematics. Amsterdam: North Holland.
Hustadt, U., and R.A. Schmidt. 2002. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning 28(2): 205–232. CrossRef
Wansing, H. 1998. Displaying modal logics. Dordrecht: Kluwer Academic Publishers.
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.
Gentzen, G. 1934. Untersuchungen über das Logische Schliessen. Mathematische Zeitschrift 39: 176–210, 405–431. CrossRef
Hähnle, R. 2001. Tableaux and related methods. In Handbook of automated reasoning, eds. A. Robinson, and A. Voronkov, pp. 101–177. Amsterdam: Elsevier.
Takano, M. 1992. Subformula property as a substitute for cut-elimination in modal propositional logics. Mathematica Japonica 37(6): 1129–1145.
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.
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.
Loveland, D.W. 1978. Automated theorem proving: A logical basis. Amsterdam: North Holland.
Avron, A. 1993. Gentzen-type systems, resolution and tableaux. Journal of Automated Reasoning 10(2): 265–281. CrossRef
Fitting, M. 1990. Destructive modal resolution. Journal of Logic and Computation 1(1): 83–97. CrossRef
Lis, Z. 1960. Wynikanie semantyczne a wynikanie formalne. Studia Logica 10: 39–60. CrossRef
Orłowska, E. 1987. Relational interpretation of modal logics. Technical Report ICSPas.
Priest, G. 2001. An introduction to non-classical logic. Cambridge: Cambridge University Press.
D’Agostino, M. et al. (eds.). 1999. Handbook of tableau methods. Dordrecht: Kluwer Academic Publishers.
Hintikka, J. 1955. Form and content in quantification theory. Acta Philosophica Fennica 8: 8–55.
Areces, C., H. DeNivelle, and M. DeRijke. 2001. Resolution in modal, description and hybrid logic. Journal of Logic and Computation 11: 717–736. CrossRef
- Other Deductive Systems
Dr. Andrzej Indrzejczak
- Springer Netherlands
- Chapter 3
Neuer Inhalt/© Filograph | Getty Images | iStock