© 2004 by Oxford University Press
Original Article |
Natural Deduction for Hybrid Logic
Department of Computer Science, Roskilde University, P.O. Box 260, DK-4000 Roskilde, Denmark. E-mail: torben{at}ruc.dk
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. Thus, we give natural deduction systems in a uniform way for a wide class of hybrid logics which appears to be impossible in the context of ordinary modal logic. We prove soundness and completeness and we prove a normalization theorem. We finally prove a result which says that normal derivations in the natural deduction system correspond to derivations in a cut-free Gentzen system.
Keywords: Hybrid logic, modal logic, natural deduction, Gentzen systems
Received 16 August 2001.
![]()
CiteULike
Connotea
Del.icio.us What's this?
This article has been cited by other articles:
![]() |
T. Brauner Adding Intensional Machinery to Hybrid Logic J Logic Computation, August 1, 2008; 18(4): 631 - 648. [Abstract] [PDF] |
||||
