article

Two Natural Deduction Systems for Hybrid Logic: A Comparison

Author:

Torben BraünerAuthors Info & Claims

Journal of Logic, Language and Information, Volume 13, Issue 1

Pages 1 - 23

https://doi.org/10.1023/A:1026187215321

Published: 01 January 2004 Publication History

Abstract

In this paper two different natural deduction systems for hybrid logic are compared and contrasted. One of the systems was originally given by the author of the present paper whereas the other system under consideration is a modified version of a natural deduction system given by Jerry Seligman. We give translations in both directions between the systems, and moreover, we devise a set of reduction rules for the latter system by translation of already known reduction rules for the former system.

References

[1]

Areces, C., Blackburn, P., and Marx, M., 2001, "Hybrid logics: Characterization, interpolation and complexity," Journal of Symbolic Logic 66, 977-1010.

[2]

Benton, N., Bierman, G.M., de Paiva, V.C.V., and Hyland, M., 1992, "Term assignment for intuitionistic linear logic," Technical Report 262, Computer Laboratory, University of Cambridge.

[3]

Benton, N., Bierman, G.M., de Paiva, V.C.V., and Hyland, M., 1993, "A term calculus for intuitionistic linear logic," pp. 75-90 in Proceedings of First International Conference on Typed Lambda Calculi and Applications, M. Bezem and J.F. Groote, eds., Lecture Notes in Computer Science, Vol. 664, Berlin: Springer-Verlag.

Digital Library

[4]

Bierman, G.M. and de Paiva, V.C.V., 2000, "On an intuitionistic modal logic," Studia Logica 65, 383-416.

[5]

Blackburn, P., 2000, "Internalizing labelled deduction," Journal of Logic and Computation 10, 137- 168.

[6]

Blackburn, P., de Rijke, M., and Venema, Y., 2001, Modal Logic, Cambridge Tracts in Theoretical Computer Science, Vol. 53, Cambridge: Cambridge University Press.

Digital Library

[7]

Braüner, T., 1996, "An axiomatic approach to adequacy," Ph.D. Thesis, Department of Computer Science, University of Aarhus, 168 pages. Published as Technical Report BRICS-DS-96-4.

[8]

Braüner, T., 2003, "Natural deduction for hybrid logic," Journal of Logic and Computation, to appear. Revised and extended version of paper in Workshop Proceedings of Methods for Modalities 2.

Digital Library

[9]

Hasle, P., Øhrstrøm, P., Braüner, T., and Copeland, J., eds., 2002, Revised and Expanded Edition of Arthur N. Prior: Papers on Time and Tense, Oxford: Oxford University Press.

[10]

Øhrstrøm, P. and Hasle, P., 1993, "A. N. Prior's rediscovery of tense logic," Erkenntnis 39, 23-50.

[11]

Prawitz, D., 1965, Natural Deduction. A Proof-Theoretical Study, Stockholm: Almqvist and Wiksell.

[12]

Prawitz, D., 1971, "Ideas and results in proof theory," pp. 235-307 in Proceedings of the Second Scandinavian Logic Symposium, J.E. Fenstad, ed., Studies in Logic and The Foundations of Mathematics, Vol. 63, Amsterdam: North-Holland.

[13]

Prior, A., 1967, Past, Present and Future, Oxford: Clarendon/Oxford University Press.

[14]

Prior, A., 1968, Papers on Time and Tense, Oxford: Clarendon/Oxford University Press.

[15]

Seligman, J., 1997, "The logic of correct description," pp. 107-135 in Advances in Intensional Logic, M. de Rijke, ed., Applied Logic Series, Dordrecht: Kluwer Academic Publishers.

[16]

Seligman, J., 2001, "Internalisation: The case of hybrid logics," Journal of Logic and Computation 11, 671-689. Special Issue on Hybrid Logics, C. Areces and P. Blackburn, eds.

[17]

Troelstra, A.S. and Schwichtenberg, H., 1996, Basic Proof Theory, Cambridge Tracts in Theoretical Computer Science, Vol. 43, Cambridge: Cambridge University Press.

Digital Library

Cited By

Braüner T(2018)Hybrid-Logical Reasoning in the Smarties and Sally-Anne TasksJournal of Logic, Language and Information10.1007/s10849-014-9206-z23:4(415-439)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1007/s10849-014-9206-z
Rybakov V(2010)Modelling of Chance Discovery in variations of Linear Temporal Logic implementing agents' interactionInternational Journal of Advanced Intelligence Paradigms10.1504/IJAIP.2010.0305352:2/3(198-219)Online publication date: 1-Dec-2010
https://dl.acm.org/doi/10.1504/IJAIP.2010.030535
Braüner T(2005)Natural Deduction for First-Order Hybrid LogicJournal of Logic, Language and Information10.1007/s10849-005-3927-y14:2(173-198)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1007/s10849-005-3927-y

Index Terms

Two Natural Deduction Systems for Hybrid Logic: A Comparison
1. Computing methodologies
  1. Artificial intelligence
    1. Knowledge representation and reasoning
      1. Nonmonotonic, default reasoning and belief revision
2. Theory of computation
  1. Logic
    1. Modal and temporal logics

Recommendations

Natural Deduction for Hybrid Logic

In this paper we give a natural deduction formulation of hybrid logic. Our natural deduction system can be extended with additional inference rules corresponding to conditions on the accessibility relations expressed by so-called geometric theories. ...
Natural Deduction for Full S5 Modal Logic with Weak Normalization

Natural deduction systems for classical, intuitionistic and modal logics were deeply investigated by Prawitz [Prawitz, D., ''Natural Deduction: A Proof-theoretical Study'', Stockholm Studies in Philosophy 3, Almqvist and Wiksell, Stockholm, 1965] from a ...
Natural Deduction for First-Order Hybrid Logic

This is a companion paper to Braüner (2004b, Journal of Logic and Computation 14 , 329--353) where a natural deduction system for propositional hybrid logic is given. In the present paper we generalize the system to the first-order case. Our natural ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Logic, Language and Information

Journal of Logic, Language and Information Volume 13, Issue 1

Winter 2004

114 pages

ISSN:0925-8531

Issue’s Table of Contents

Copyright © Copyright © 2004 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 January 2004

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 05 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Braüner T(2018)Hybrid-Logical Reasoning in the Smarties and Sally-Anne TasksJournal of Logic, Language and Information10.1007/s10849-014-9206-z23:4(415-439)Online publication date: 24-Dec-2018
https://dl.acm.org/doi/10.1007/s10849-014-9206-z
Rybakov V(2010)Modelling of Chance Discovery in variations of Linear Temporal Logic implementing agents' interactionInternational Journal of Advanced Intelligence Paradigms10.1504/IJAIP.2010.0305352:2/3(198-219)Online publication date: 1-Dec-2010
https://dl.acm.org/doi/10.1504/IJAIP.2010.030535
Braüner T(2005)Natural Deduction for First-Order Hybrid LogicJournal of Logic, Language and Information10.1007/s10849-005-3927-y14:2(173-198)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1007/s10849-005-3927-y

View Options

View options

Figures

Tables

Media

View Issue’s Table of Contents