Alladi Ramakrishnan Hall

Hybrid Logic and its Proof-Theory

Torben Braüner

Roskilde University, Denmark

Hybrid logic is an extension of ordinary modal logic which allows explicit reference to individual points in a model (where the points represent times, possible worlds, states in a computer, or something else). This additional expressive power is useful for many applications, for example when reasoning about time one often wants to formulate a series of statements about what happens at specific times, and standard modal logics do not allow this.

There is little consensus about proof-theory for ordinary modal logic. Many modal-logical proof systems lack important properties and the relationships between proof systems for different modal logics are often unclear. In my talk I will demonstrate that these deficiencies are remedied by hybrid-logical proof-theory.

In my talk I first give a brief introduction to hybrid logic and its origin in Arthur Prior's temporal logic. I then describe essential proof-theoretical results for a natural deduction formulation of hybrid logic. The natural deduction system is extended with additional inference rules corresponding to conditions on the model expressed by what are called geometric theories. Thus, I give natural deduction systems in a uniform way for a wide class of hybrid logics.