Modal Hybrid Logic
DOI:
https://doi.org/10.12775/LLP.2007.006Keywords
modal logics, tense logics, hybrid logics, correspondence theory, proof methodsAbstract
This is an extended version of the lectures given during the 12-th Conference on Applications of Logic in Philosophy and in the Foundations of Mathematics in Szklarska Poręba (7–11 May 2007). It contains a survey of modal hybrid logic, one of the branches of contemporary modal logic. In the first part a variety of hybrid languages and logics is presented with a discussion of expressivity matters. The second part is devoted to thorough exposition of proof methods for hybrid logics. The main point is to show that application of hybrid logics may remarkably improve the situation in modal proof theory.References
Abadi, M. and Z. Manna, ‘Nonclausal Deduction in First-Order Temporal Logic', Journal of the Assoc. Comput. Mach. 37: 279–317, 1990.
D’Agostino, M., ‘Tableau Methods for Classical Propositional Logic', in: M. D’Agostino et al. (eds.), Handbook of Tableau Methods, pp. 45–123, Kluwer Academic Publishers, Dordrecht 1999.
Allen, J., ‘Towards a general theory of Knowledge and Action', Artificial Intelligence, 23:123–154, 1984.
Anderson, A., R. and N., D. Belnap, Entailment: the Logic of Relevance and Necessity, vol I Princeton University Press, Princeton 1975.
Areces, C., P. Blackburn, and M. Marx, ‘The Computational Complexity of Hybrid Temporal Logics’, Logic Journal of the IGPL, 8(5):653–679, 2000.
Areces, C., P. Blackburn, and M. Marx, ‘Hybrid Logics: Characterization, Interpolation and Complexity’, Journal of Symbolic Logic, 66: 977–1010, 2001.
Areces, C., H. DeNivelle, and M. DeRijke, ‘Resolution in Modal, Description and Hybrid Logic’, Journal of Logic and Computation, 11: 717–736, 2001.
Areces, C., J. Heguiabehere, ‘HyLoRes: Direct Resolution for Hybrid Logics’, available on Hybrid Logic Homepage.
Areces, C., D. Gorin, ‘Ordered resolution with selection for h(@)’, in: F. Baader, and A. Voronkov (eds.) Proceedings of LPAR 2004, pp. 125–141, LNCS 3452, 2005.
Areces, C., B. ten Cate, ‘Hybrid Logics’, in: P. Blackburn, J. van Benthem, and F. Wolter (eds.) Handbook of Modal Logic, pp. 821–868, Elsevier 2006.
Avron, A., ‘Gentzen-type systems, Resolution and Tableaux’, Journal of Automated Reasoning 10/2: 265–281, 1993.
Avron, A., F. Honsell, M. Miculan and C. Paravano, ‘Encoding Modal Logics in Logical Frameworks’, Studia Logica 60:161–202, 1998.
Basin, D., S. Mathews, and L. Vigano, ‘Labelled Propositional Modal Logics: Theory and Practice’, Journal of Logic and Computation 7 (6): 685–717, 1997.
Basin, D., S. Mathews, and L. Vigano, ‘Natural Deduction for Non-Classical Logics’, Studia Logica 60: 119–160, 1998.
Belnap, N., D. ‘Display Logic’, Journal of Philosophical Logic, 11:375–417, 1982.
Blackburn, P. Nominal Tense Logic and other Sorted Intensional Frameworks, Ph.D thesis, Centre for Cognitive Science, University of Edinburgh, 1990.
Blackburn, P., ‘Nominal Tense Logic’, Notre Dame Journal of Formal Logic, 34: 56–83, 1992.
Blackburn, P., ‘Tense, temporal reference and tense logic’, Journal of Semantics, 11:83–101, 1994.
Blackburn, P., ‘Internalizing Labelled Deduction’, Journal of Logic and Computation, 10(1): 137–168, 2000.
Blackburn, P., ‘Representation, Reasoning, and Relational Structures: a Hybrid Logic Manifesto’, Logic Journal of the IGPL, 8 (3): 339–365, 2000.
Blackburn, P., ‘Fine Grained Theories of Time’, in: H. Wansing (ed.) Non-Classical Logic, King’s College University Press, 2001.
Blackburn, P., M. DeRijke, and Y. Venema, Modal Logic, Cambridge University Press, Cambridge 2001.
Blackburn, P., M. Marx, ‘Tableaux for Quantified Hybrid Logic’, in: U. Egly, C. Fermuller (eds.), Tableaux 2002, LNAI 2381, pp. 38–52.
Blackburn, P., J. Seligman, ‘Hybrid Languages’, Journal of Logic, Language and Information, 4: 251–272, 1995.
Blackburn, P., M. Tzakova, ‘Hybrid Completeness’, Logic Journal of the IGPL, 6 (4): 625–650, 1998.
Blackburn, P., M. Tzakova, ‘Hybrid Languages and Temporal Logic’, Logic Journal of the IGPL, 7 (1): 27–54, 1999.
Blackburn, P., B. ten Cate, ‘Beyond Pure Axioms: Node Creating Rules in Hybrid Tableaux’, in: C. Areces et all (eds.) Hybrid Logics, pp. 21–35, 2002.
Blackburn, P., B. ten Cate, ‘Pure Extensions, Proof Rules and Hybrid Axiomatics’, Studia Logica 75, 3: 345–376, 2006.
Boolos, G., ‘Don’t eliminate Cut’, Journal of Philosophical Logic, 7: 373–378, 1984.
Braüner, T., ‘Natural Deduction for Hybrid Logic’, Journal of Logic and Computation 14/3: 329–353, 2004.
Bull, R., ‘An approach to Tense Logic’, Theoria 36:282–300, 1970.
Bull, R. and K. Segerberg ‘Basic Modal Logic’, in: D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, vol II, pp. 1–88, Reidel Publishing Company, Dordrecht 1984.
Burgess, J.,P., ‘Basic Tense Logic’, in: D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, vol II, pp. 89–133, Reidel Publishing Company, Dordrecht 1984.
Carnielli, W.,A., ‘On Sequents and Tableaux for Many-valued Logics’, Journal of Non-Classical Logic 8 (1): 59–76, 1991.
Chang, C.,L. and R.,C.,T., Lee, Symbolic Logic and Mechanical Theorem Proving, Academic Press, Orlando 1973.
Chellas, B., Modal Logic, Cambridge University Press, Cambridge 1980.
Davis, M. and H. Putnam, ‘A Computing Procedure for Quantification Theory’, Journal of the Assoc. Comput. Mach. 7:201–215, 1960.
Demri, S. ‘Sequent Calculi for Nominal Tense Logics: a step towards mechanization?’, in: N. Murray (ed.), Tableaux 99, LNAI 1617, pp. 140–154, Springer, Berlin 1999.
Demri, S. and R. Goré, ‘Cut-free Display Calculi for Nominal Tense Logics’, in: N. Murray (ed.), Tableaux 99, LNAI 1617, pp. 155–170, Springer, Berlin 1999.
Farinas del Cerro, L. and A. Herzig, ‘Modal Deduction with Applications in Epistemic and Temporal Logics’, in: D. Gabbay et all. (eds.) Handbook of Logic in Artificial Intelligence and Logic Programming, vol IV, pp. 499–594, Clarendon Press, Oxford 1995.
Fitch, F., Symbolic Logic, Ronald Press Co, New York 1952.
Fitch, F., ‘Tree Proofs in Modal Logic (abstract)’, The Journal of Symbolic Logic, 31:152, 1966.
Fitch, F., ‘Natural Deduction Rules for Obligation’, American Philosophical Quaterly, 3:27–38, 1966.
Fitting, M., ‘Tableau methods of proof for Modal Logics’, Notre Dame Journal of Formal Logic, 13 (2): 237–247, 1972.
Fitting, M., Proof Methods for Modal and Intuitionistic Logics, Reidel, Dordrecht 1983.
Fitting, M., ‘Destructive Modal Resolution’, Journal of Logic and Computation, 1(1):83–97, 1990.
Fitting, M., First-Order Logic and Automated Theorem Proving, Springer, Berlin 1996.
Fitting, M., R., L. Mendelsohn, First-Order Modal Logic, Kluwer, Dordrecht 1998.
Gabbay, D., ‘An Irreflexivity Lemma with Applications to Axiomatizations of Conditions on Linear Frames’, in: U. Munnich, (ed.) Aspects of Philosophical Logic, pp. 67–89, Reidel 1981.
Gabbay, D., LDS - Labelled Deductive Systems, Clarendon Press, Oxford 1996.
Gabbay, D., A. Kurucz, F. Wolter, M. Zakharyaschev, Many-Dimensional Modal Logics: Theory and Applications, Elsevier 2003.
Gallier, J.,H., Logic for Computer Science, Harper and Row, New York 1986.
Gargov, G., V. Goranko ‘Modal Logic with Names’, Journal of Philosophical Logic, 22:607–636, 1993.
Gentzen, G., ‘Untersuchungen über das Logische Schliessen’, Mathematische Zeitschrift 39: 176–210 and 39: 405–431, 1934.
Gentzen, G., ‘Die Widerspruchsfreiheit der reinen Zahlentheorie’, Mathematische Annalen 112: 493–565, 1936.
Goldblatt, R. I. Logics of Time and Computation, CSLI Lecture Notes, Stanford 1987.
Goranko, V., ‘Refutation Systems in Modal Logic’, Studia Logica 53/2: 229–234, 1994.
Goranko, V., ‘Temporal Logic with reference pointers’, in: Temporal Logic, LNiAI 827, pp. 133–148, Springer 1994.
Goranko, V., D. Vakarelov, ‘Sahlqvist formulas in hybrid polyadic modal logics’, Journal of Logic and Computation 11/5: 737–754, 2001.
Goré, R. Cut-free Sequent and Tableau Systems for Propositional Normal Modal Logics, PhD thesis, University of Cambridge, 1992.
Goré, R. ‘Tableau Methods for Modal and Temporal Logics’, in: M. D’Agostino et al. (eds.), Handbook of Tableau Methods, pp. 297–396, Kluwer Academic Publishers, Dordrecht 1999.
Hähnle, R. Automated Deduction in Multiple-Valued Logics, Oxford University Press, 1994.
M. D’Agostino et all (ed.), Handbook of Tableau Methods, Kluwer Academic Publishers, Dordrecht 1999.
Hawthorn, J., ‘Natural Deduction in Normal Modal Logic’, Notre Dame Journal of Formal Logic 31: 263–273, 1990.
Hemaspaandra, E., ‘The Price of Universality’, Notre Dame Journal of Formal Logic 37:174–203, 1996.
Horrocks, I. Optimising Tableaux Decision Procedures for Description Logics, PhD Thesis, University of Manchester 1997.
Horrocks, I., U. Satler, and S. Tobies, ‘Practical Reasoning for Very Expressive Description Logics', Logic Journal of the IGPL 8 (3): 239–263, 2000.
Hustadt, U. and R.,A. Schmidt, ‘Issues of decidability for Description logics in the framework of resolution’, in: R. Caferra and G. Salzer (eds.), Automated Deduction in Classical and Non-Classical Logics, pp. 192–206, Springer 2000.
Hustadt, U. and R.,A. Schmidt, ‘Using Resolution for Testing Modal Satisfiability and building Models’, Journal of Automated Reasoning 28(2): 205–232, 2002.
Indrzejczak, A., ‘Natural Deduction System for Tense Logics’, Bulletin of the Section of Logic 23 (4): 173–179, 1994.
Indrzejczak, A., ‘Cut-free Sequent Calculus for S5’, Bulletin of the Section of Logic 25 (2): 95–102, 1996.
Indrzejczak, A., ‘Generalised Sequent Calculus for Propositional Modal Logics’, Logica Trianguli 1: 15–31, 1997.
Indrzejczak, A., ‘A Survey of Natural Deduction Systems for Modal Logics’, Logica Trianguli 3: 55–84, 1999.
Indrzejczak, A., ‘Multiple Sequent Calculus for Tense Logics’, Abstracts of AiML and ICTL 2000: 93–104, Leipzig 2000.
Indrzejczak, A., ‘Decision Procedure for Modal Logics in Natural Deduction setting’, unpublished version, Łódź 2001.
Indrzejczak, A., ‘Hybrid system for (not only) Hybrid Logic’, Abstracts of AiML 2002: 137–156, Toulouse 2002.
Indrzejczak, A., ‘Labelled Analytic Tableaux for S4.3.’, Bulletin of the Section of Logic 31 (1): 15–26, 2002.
Indrzejczak, A., ‘Resolution based Natural Deduction’, Bulletin of the Section of Logic 31 (3): 159–170, 2002.
Indrzejczak, A., ‘A Labelled Natural Deduction System for Linear Temporal Logic’, Studia Logica 75/3: 345–376, 2003.
Indrzejczak, A., ‘Introduction to methodology of Sequent Calculi’, unpublished manuscript in polish, 2006.
Jaśkowski, S., ‘On the Rules of Suppositions in Formal Logic', Studia Logica 1: 5–32, 1934.
Kalish, D., and R. Montague, ‘Remarks on Descriptions and Natural Deduction’, Archiv. für Mathematische Logik und Grundlagen Forschung 3: 50–64, 65–73, 1957.
Kalish, D., and R. Montague, Logic, Techniques of Formal Reasoning, Harcourt, Brace and World, New York 1964.
Konikowska, B., ‘A logic for reasoning about relative similarity', Studia Logica 58 (1): 185–226, 1997.
Kracht, M., ‘Power and Weakness of the Modal Display Calculus’, in: H. Wansing (ed.) Proof Theory of Modal Logic, pp. 93–121, Kluwer, Dordrecht 1996.
Kripke, S., ‘A Completeness Theorem in Modal Logic’, Journal of Symbolic
Logic 24: 1–14, 1959.
Marx, M., S. Mikulas, and M. Reynolds, ‘The Mosaic Method for Temporal Logics’, in: R. Dyckhoff (ed.) Automated Reasoning with Analytic Tableaux and Related Methods, Proc. of International Conference TABLEAUX 2000, Saint Andrews, Scotland, LNAI 1847:324–340, Springer 2000.
Massacci, F., ‘Strongly Analytic Tableaux for Normal Modal Logics’, in: A. Bundy (ed.) Proc. CADE-12, LNAI 814: 723–737, Springer 1994.
Massacci, F., ‘Single Step Tableaux for Modal Logics: methodology, computations, algorithms’, Technical Report TR-04, Dipartimento di Informatica e Sistemistica, Universita di Roma “La Sapienza” 1998.
McCarthy, J., P. Hayes, ‘Some philosophical problems from the standpoint of Artificial Inteligence’, in: B. Meltzer, D. Michie (ed.) Machine Intelligence 4, Edinburgh University Press 1969.
De Nivelle, H., R.,A. Schmidt, and U. Hustadt, ‘Resolution-based Methods for Modal Logics’, Logic Journal of the IGPL, 8/3: 265–292, 2000.
Ohnishi, M., K. Matsumoto, ‘Gentzen Method in Modal Calculi I’, Osaka Mathematical Journal 9: 113–130, 1957.
Ohnishi, M., K. Matsumoto, ‘Gentzen Method in Modal Calculi II’, Osaka Mathematical Journal 11: 115–120, 1959.
Ohrstrom, P., P. Hasle, ‘A.N. Prior Rediscovery of Tense Logic’, Erkenntniss 39: 23–50, 1993.
Orłowska, E. ‘Relational interpretation of Modal Logics’, Technical Report ICSPas 1987.
Passy, S., T. Tinchev, ‘PDL with data constants’, Information Processing Letters 20: 35–41, 1985.
Passy, S., T. Tinchev, ‘An essay in CDL’, Information and Computation 93: 263–332, 1991.
Perzanowski, J., ‘Logiki modalne a filozofia’, in: J. Perzanowski (ed.) Jak filozofować, pp. 262–346, PWN, Warszawa 1989.
Perzanowski, J., ‘Combination Semantics for Intensional Logics I’, Logique et Analyse 165–166: 181–203, 1999.
Perzanowski, J., ‘Towards Combination Metaphysics’, Reports on Mathematical Logic, 38:93–116, 2004.
Prawitz, D. Natural Deduction, Almqvist and Wiksell, Stockholm 1965.
Prior, A. Time and Modality, Oxford University Press, Oxford 1957.
Prior, A. Past, Present and Future, Clarendon/Oxford University Press, Oxford 1967.
Prior, A. Papers on Time and Tense, Clarendon/Oxford University Press, Oxford 1968.
Rescher, N., and A. Urquhart, Temporal Logic, Springer-Verlag, New York 1971.
Robinson, J.,A., ‘A Machine Oriented Logic based on the Resolution Principle’, Journal of the Assoc. Comput. Mach., 12: 23–41, 1965.
Russo, A., ‘Modal Labelled Deductive Systems’, Dept. of Computing, Imperial College, London, Technical Report 95/7, 1995.
Schmidt, R.,A., ‘Developing Modal Tableaux and Resolution Methods via First-Order Resolution‘ in: M. de Rijke (ed.) Advances in Modal Logic 6, pp. 107–135. Kluwer 2006.
Seligman, J., ‘A cut-free sequent calculus for elementary situated reasoning’, Technical Report HCRC/RP-22 HCRC, Edinburgh, 1991.
Seligman, J., ‘Situated Consequence in Elementary Situation Theory’, Logic Group Preprint IULG-92-16, Indiana University, 1992.
Seligman, J., ‘The Logic of Correct Description‘ in: M. de Rijke (ed.) Advances in Intensional Logic, pp. 107–135. Kluwer 1997.
Seligman, J., ‘Internalization: The Case of Hybrid Logics’, Journal of Logic and Computation, 11: 671–689, 2001.
Simpson, A. The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh, 1994.
Smullyan, R., First-Order Logic, Springer, Berlin 1968.
ten Cate, B. Model Theory for Extended Modal Languages, PhD thesis, University of Amsterdam, 2004.
Thomason, R., H., ‘A Fitch-style formulation of Conditional Logic’, Logique et Analyse 13: 397–412, 1970.
Tzakova, M., ‘Tableau Calculi for Hybrid Logics’, in: N. Murray (ed.) Conference on Tableaux Calculi and Related Methods (TABLEAUX), Saratoga Springs, USA, LNAI 1617 pp. 278–292, 1999.
Vickers, S., Topology via Logic, Cambridge University Press, Cambridge 1988.
Wansing, H., Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht 1999.
Wansing, H., ‘Sequent Systems for Modal Logics’, in: D. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic, vol IV, pp. 89–133, Reidel Publishing Company, Dordrecht 2002.
Zeman, J.,J., Modal Logic, Oxford University Press, Oxford 1973.
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 647
Number of citations: 0
