# Hybrid Logic

*First published Tue Jun 13, 2006; substantive revision Thu Sep 22, 2011*

The term Hybrid Logic covers a number of logics obtained by adding further expressive power to ordinary modal logic. The most basic hybrid logic is obtained by adding so-called nominals which are propositional symbols of a new sort, each being true at exactly one possible world. The history of hybrid logic goes back to Arthur N. Prior's work in the 1960s.

## 1. Motivations for hybrid logic

In the standard Kripke semantics for modal logic, truth is relative to points in a set. Thus, a propositional symbol might have different truth-values relative to different points. Usually, these points are taken to represent possible worlds, times, space, knowledge, states in a computer, or something else. This allows us to formalize natural language statements whose truth-values are relative to for example times, like the statement

it is raining

which has clearly different truth-values at different times. Now, certain natural language statements are true at exactly one time, possible world, or something else. An example is the statement

it is five o'clock 15 March 2006

which is true at the time five o'clock 15 March 2006, but false at all other times. The first kind of natural language statements can be formalized in ordinary modal logic, but the second kind cannot.

A major motivation for hybrid logic is to add further expressive power
to ordinary modal logic with the aim of being able to formalize the
second kind of statements. This is obtained by adding to ordinary
modal logic a second sort of propositional symbols called
*nominals* such that in the Kripke semantics each nominal is
true relative to exactly one point. A natural language statement of
the second kind (like the example statement with the time five
o'clock 15 March 2006) is then formalized using a nominal, not
an ordinary propositional symbol (which would be used to formalize the
example statement with rainy weather). The fact that a nominal is true
relative to exactly one point implies that a nominal can be considered
a term referring to a point, for example, if *a* is a nominal
that stands for “it is five o'clock 15 March 2006”, then the
nominal *a* can be considered a term referring to the time five
o'clock 15 March 2006. Thus, in hybrid logic a term is a
specific sort of propositional symbol whereas in first-order logic it
is an argument to a predicate.

Most hybrid logics involve further additional machinery than
nominals. There is a number of options for adding further machinery;
here we shall consider so-called *satisfaction operators*. The
motivation for adding satisfaction operators is to be able to
formalize a statement being true at a particular time, possible world,
or something else. For example, we want to be able to formalize that
the statement “it is raining” is true at the time five o'clock 15
March 2006, that is, that

at five o'clock 15 March 2006, it is raining.

This is formalized by the formula *a*:*p* where the nominal
*a* stands for “it is five o'clock 15 March 2006”
as above and where *p* is an ordinary propositional symbol that
stands for “it is raining”. It is the part *a*: of
the formula
*a*:*p* that is called a satisfaction operator. In general, if
*a* is a nominal and *φ* is an arbitrary formula, then a
new formula *a*:*φ* called a *satisfaction
statement* can be built (sometimes the notation
*@** _{a}* is used instead of

*a*:). The satisfaction statement

*a*:

*φ*expresses that the formula

*φ*is true relative to one particular point, namely the point to which the nominal

*a*refers.

To sum up, we have now added further expressive power to ordinary
modal logic in the form of nominals and satisfaction operators.
Informally, the nominal *a* has the truth-condition

ais true relative toapointw

if and only if

the reference ofais identical tow

and the satisfaction statement *a*:*φ* has the
truth-condition

a:φis true relative to a pointw

if and only if

φis true relative to the reference ofa

Note that actually the point *w* does not matter in the
truth-condition for *a*:*φ* since the satisfaction
operator *a*: moves the point of evaluation to the reference of
*a* whatever the identity of *w*.

It is remarkable that nominals together with satisfaction operators
allow us to express that two points are identical: If the nominals
*a* and *b* refer to the points *w* and
*v*, then the formula *a*:*b* expresses that
*w* and *v* are identical. The following line of
reasoning shows why.

a:bis true relative to a pointw

if and only ifbis true relative to the reference ofa

if and only ifbis true relative tow

if and only if the reference ofbis identical tow

if and only ifvis identical tow

The identity relation on a set has the well-known properties reflexivity, symmetry, and transitivity, which is reflected in the fact that the formulas

a:a

a:b→b:a

(a:b&b:c) →a:c

are valid formulas of hybrid logic. Also the formula

(a:b&a:φ) →b:φ

is valid. This is the rule of replacement.

Beside nominals and satisfaction operators, in what follows we shall
consider the so-called *binders* ∀ and ↓ allowing
us to build formulas ∀*a**φ* and
↓*a**φ*. The binders bind nominals to points in
two different ways: The ∀ binder quantifies over points
analogous to the standard first-order universal quantifier, that is,
∀*a**φ* is true relative to *w* if and
only if whatever point the nominal a refers to, it is the case that
*φ* is true relative to *w*. The ↓ binder binds
a nominal to the point of evaluation, that is,
↓*a**φ* is true relative to *w* if and
only if *φ* is true relative to w when a refers to
*w*. It turns out that the ↓ binder is definable in terms
of ∀ (as shown below).

## 2. Formal semantics

The language we consider is the language of ordinary modal logic built
over ordinary propositional symbols *p*, *q*,
*r*, … as well as nominals *a*, *b*,
*c*, … and extended with satisfaction operators and
binders. We take the propositional connectives & and ¬ to be
primitive; other propositional connectives are defined as
usual. Similarly, we take the modal operator □ to be primitive
and define the modal operator ◊ as ¬□¬. As the
name suggests, binders bind nominals and the notions of free and bound
occurrences of nominals are defined analogously to first-order logic.
Satisfaction operators do not bind nominals, that is, the free nominal
occurrences in a formula *a:**φ* are the free
nominal occurrences in *φ* together with the occurrence of
a. We let *φ*[*c*/*a*] be the formula
*φ* where the nominal *c* has been substituted for
all free occurrences of the nominal *a*. If the
nominal *a* occurs free in *φ* within the scope of
∀*c* or ↓*c*, then the bound
nominal *c* in *φ* is renamed as appropriate.

We now define models and frames. A *model* for hybrid logic is
a triple (*W*, *R*, *V*) where *W* is a
non-empty set, *R* is a binary relation on *W*, and
*V* is a function that to each pair consisting of an element of
*W* and an ordinary propositional symbol assigns an element of
the set {0,1}. The pair (*W*, *R*) is called a
*frame*. Thus, models and frames are the same as in ordinary
modal logic. The elements of *W* are called *worlds* and
the relation *R* is called the *accessibility
relation*. The model (*W*, *R*, *V*) is said to
be *based* on the frame (*W*, *R*).

An *assignment* for a model *M* =
(*W*, *R*, *V*) is a function *g* that to
each nominal assigns an element of *W*. An assignment g′
is an *a**-variant* of *g* if g′ agrees
with *g* on all nominals save possibly *a*. The relation
*M*, *g*, *w*
⊨ *φ*
is defined by induction, where *g* is an assignment,
*w* is an element of *W*, and *φ* is a
formula.

M,g,w⊨piffV(w,p)=1

M,g,w⊨aiffw=g(a)

M,g,w⊨φ&ψiffM,g,w⊨φandM,g,w⊨ψ

M,g,w⊨ ¬φiff notM,g,w⊨φ

M,g,w⊨ □φiff for any elementvofWsuch thatwRv, it is the case thatM,g,w⊨φ

M,g,w⊨a:φiffM,g,g(a) ⊨φ

M,g,w⊨ ∀aφiff for anya-variantg′ ofg, it is the case thatM,g′,w⊨φ

M,g,w⊨ ↓aφiffM,g′,w⊨φwhereg′ is thea-variant ofgsuch thatg′(a) =w.

A formula *φ* is said to be *true* at *w* if
*M*, *g*, *w*
⊨ *φ*;
otherwise it is said to be *false* at *w*. By
convention *M*, *g*
⊨ *φ* means
*M*, *g*, *w*
⊨ *φ* for every
element *w* of *W* and *M*
⊨ *φ* means
*M*, *g*
⊨ *φ* for every
assignment *g*. A formula *φ* is *valid* in a
frame if and only if *M*
⊨ *φ* for any model
*M* that is based on the frame in question. A formula
*φ* is *valid* in a class of frames *F* if
and only if *φ* is valid in any frame in *F*. A
formula *φ* is *valid* if and only if *φ*
is valid in the class of all frames. The definition of satisfiability
is left to the reader.

Note that the binder ↓ is definable in terms of ∀ as the
formula ↓*a**φ* ↔
∀*a*(*a* → *φ*) is valid in any
frame.

The fact that hybridizing ordinary modal logic actually does give more
expressive power can for example be seen by considering the formula
↓*c*□¬*c*. It is straightforward to
check that this formula is valid in a frame if and only if the frame
is irreflexive. Thus, irreflexivity can be expressed by a
hybrid-logical formula, but it is well known that it cannot be
expressed by any formula of ordinary modal logic. Irreflexivity can
actually be expressed just by adding nominals to ordinary modal logic,
namely by the formula *c**→*□¬*c*.
Other examples of properties expressible in hybrid logic, but not in
ordinary modal logic, are asymmetry (expressed by
*c**→*□¬◊*c*), antisymmetry
(expressed by
*c**→*□(◊*c**→**c*)),
and universality (expressed by ◊*c*).

## 3. Translations

Hybrid logic can be translated into first-order logic with equality,
and (a fragment of) first-order logic with equality can be translated
back into (a fragment of) hybrid logic. The first-order language under
consideration has a 1-place predicate symbol *p****
corresponding to each ordinary propositional symbol *p* of modal
logic, a 2-place predicate symbol *R*, and a 2-place predicate
symbol =. Of course, the predicate symbol *p****
will be interpreted such that it relativises the interpretation of the
corresponding modal propositional symbol *p* to worlds, the
predicate symbol *R* will be interpreted using the accessibility
relation, and the predicate symbol = will be interpreted using
the identity relation on worlds. We let *a*, *b*,
*c*, … range over first-order variables. The language
does not have constant or function symbols. We shall identify
first-order variables with nominals of hybrid logic.

We first translate hybrid logic into first-order logic with
equality. Given two new first-order variables *a* and
*b*, the translations ST* _{a}* and
ST

*are defined by mutual recursion. We just give the translation ST*

_{b}*.*

_{a}ST(_{a}p) =p*(a)

ST(_{a}c) =a=c

ST(_{a}φ&ψ) = ST(_{a}φ) & ST(_{a}ψ)

ST(¬_{a}φ) = ¬ST(_{a}φ)

ST(□_{a}φ) = ∀b(R(a,b) → ST(_{b}φ))

ST(_{a}c:φ) = ST(_{a}φ)[c/a]

ST(↓_{a}cφ) = ST(_{a}φ)[a/c]

ST(∀_{a}cφ) = ∀cST(_{a}φ)

The definition of ST* _{b}* is obtained by exchanging

*a*and

*b*. The translation is an extension of the well-known

*standard translation*from modal logic into first-order logic. As an example, we demonstrate step by step how the hybrid-logical formula ↓

*c*□¬

*c*is translated into a first-order formula:

ST (↓_{a}c□¬c)= ST (□¬_{a}c)[a/c]= ∀ b(R(a,b) → ST(¬_{b}c))[a/c]= ∀ b(R(a,b) → ¬ST(_{b}c))[a/c]= ∀ b(R(a,b) → ¬b=c)[a/c]= ∀ b(R(a,b) → ¬b=a).

The resulting first-order formula is equivalent to
¬*R*(*a*, *a*) which shows that
↓*c*□¬*c* indeed does correspond to the
accessibility relation being irreflexive, cf.
above.

First-order logic with equality can be translated back into hybrid logic by the translation HT given below.

HT(p*(a)) =a:p

HT(R(a,c)) =a:◊c

HT(a=c) =a:c

HT(φ&ψ) = HT(φ) & HT(ψ)

HT(¬φ) = ¬HT(φ)

HT(∀aφ) = ∀aHT(φ)

Note that the hybrid-logical binder ∀ is needed. The history of the above mentioned observations goes back to the work of Arthur N. Prior, we shall return to that later.

Similarly, the so-called *bounded fragment* of first-order
logic can be translated into the hybrid logic but here only the binder
↓ is needed, as pointed out in the paper Areces, Blackburn, and
Marx (2001). The bounded fragment is the fragment of first-order logic
with the property that quantifiers only occur as in the formula
∀*c*(*R*(*a*, *c*) →
*φ*), where it is required that the variables *a*
and *c* are different. A translation from the bounded fragment
to the hybrid logic without the ∀ binder can be obtained by
replacing the last clause in the translation HT above by

HT(∀c(R(a,c) →φ)) =a:□↓cHT(φ).

In Areces, Blackburn, and Marx (2001) a number of independent semantic characterisations of the bounded fragment are given.

The translations given above are truth-preserving. To state this
formally, one makes use of the well-known observation that models and
assignments for hybrid logic can be considered as models and
assignments for first-order logic and vice versa. These
truth-preservation results are straightforward to formulate and we
leave the details to the reader. Thus, the hybrid logic with the
binder ∀ has the same expressive power as first-order logic
with equality and the hybrid logic without the binder ∀ (but
with the binder ↓) has the same expressive power as the bounded
fragment of first-order logic (note that the translation
ST* _{a}*(

*φ*) of any formula

*φ*without the binder ∀ is in the bounded fragment).

## 4. Arthur N. Prior and hybrid logic

The history of hybrid logic goes back to Arthur N. Prior's hybrid
tense logic, which is a hybridized version of ordinary tense logic.
With the aim of investigating this further, we shall give a formal
definition of hybrid tense logic: The language of hybrid tense logic is
simply the language of hybrid logic defined above except that there are
two modal operators, namely *G* and *H*, instead of the
single modal operator □. The two new modal operators are
called *tense operators*. The semantics of hybrid tense logic is
the semantics of hybrid logic, cf. earlier, with the clause for □
replaced by clauses for the tense operators *G* and
*H*.

M,g,w⊨Gφiff for any elementvofWsuch thatwRv, it is the case thatM,g,w⊨φ

M,g,w⊨Hφiff for any elementvofWsuch thatvRw, it is the case thatM,g,w⊨φ

Thus, there are now two modal operators, namely one that “looks
forwards” along the accessibility relation and one that
“looks backwards”. In tense logic the elements of the set
*W* are called *moments* or *instants* and the
relation *R* is called the *earlier-later relation*.

Of course, it is straightforward to modify the translations
ST* _{a}* and HT above such that translations are
obtained between hybrid tense logic (including the ∀ binder)
and first-order logic with equality. The first-order logic under
consideration is what Prior called

*first-order earlier-later logic*. Given the translations, it follows that Prior's first-order earlier-later logic has the same expressive power as hybrid tense logic.

Now, Prior introduced hybrid tense logic in connection with what he called four grades of tense-logical involvement. The motivation for his four grades of tense-logical involvement was philosophical. The four grades were presented in the book Prior (1968), Chapter XI (also Chapter XI in the new edition Prior (2003)). Moreover, see Prior (1967), Chapter V.6 and Appendix B.3-4. For a more general discussion, see the posthumously published book Prior and Fine (1977). The stages progress from what can be regarded as pure first-order earlier-later logic to what can be regarded as pure tense logic; the goal being to be able to consider the tense logic of the fourth stage as encompassing the earlier-later logic of the first stage. In other words, the goal was to be able to translate the first-order logic of the earlier-later relation into tense logic. It was with this goal in mind Prior introduced so-called instant-propositions:

What I shall call the third grade of tense-logical involvement consists in treating the instant-variablesa,b,c, etc. as also representing propositions. (Prior 1968, p. 122-123)

In the context of modal logic, Prior called such propositions
possible-world-propositions. Of course, this is what we here call
nominals. Prior also introduced the binder ∀ and what we here
call satisfaction operators (he used the notation
*T*(*a*, *φ*) instead of
*a*:*φ* for satisfaction operators). In fact,
Prior's third grade tense logic is identical to the hybrid tense logic
as defined above. The ↓ binder was introduced much later. Thus,
Prior obtained the expressive power of his first-order earlier-later
logic by adding to ordinary tense logic further expressive power in
the form of nominals, satisfaction operators, and the binder
∀. So from a technical point of view he clearly reached his
goal.

However, from a philosophical point of view it has been debated whether or not the ontological import of his third grade tense logic is the same as the ontological import of the first-order earlier-later logic. For example, the ∀ binder is by some authors considered a direct analogy to the first-order ∀ quantifier, and therefore suspect; see for example the paper Sylvan (1996) in the collection Copeland (1996). Also a number of other papers in this collection are relevant. See Braüner (2002) for a discussion of Prior's fourth grade tense logic. See also Øhrstrøm and Hasle (1993), Øhrstrøm and Hasle (2006), Müller (2007), and Blackburn (2007). Finally, see the discussion of Prior's work in the book Braüner (2011).

## 5. The development of hybrid logic since Prior

The first completely rigorous definition of hybrid logic was given in
Robert Bull's paper Bull (1970) which appeared in a special issue of
the journal *Theoria* in memory of Prior. Bull introduces a
third sort of propositional symbols where a propositional symbol is
assumed to be true exactly at one branch (“course of events”) in a
branching time model. This idea of sorting propositional symbols
according to restrictions on their interpretations has later been
developed further by a number of authors, see Section 5 of the paper
Blackburn and Tzakova (1999) for a discussion.

The hybrid logical machinery originally invented by Prior in the late 1960s was reinvented in the 1980s by Solomon Passy and Tinko Tinchev from Bulgaria, see Passy and Tinchev (1985) as well as Passy and Tinchev (1991). Rather than ordinary modal logic, this work took place in connection with the much more expressive Propositional Dynamic Logic.

A major contribution in the 1990s was the introduction of the ↓ binder by Valentin Goranko, see the papers Goranko (1994) and Goranko (1996). Since then, hybrid logic with the ↓ binder has been extensively studied by a number of people, notably Patrick Blackburn and his collaborators, see for example the paper Areces, Blackburn, and Marx (2001) on model-theoretic aspects of this logic. A recent very comprehensive study of the model-theory of hybrid logic is the PhD thesis of ten Cate (2004).

Also the weaker hybrid logic obtained by omitting both of the binders ↓ and ∀ has been the subject of extensive exploration. It turns out that this binder-free logic and a number of variants of it are decidable. In the paper Areces, Blackburn, and Marx (1999), a number of complexity results are given for hybrid modal and tense logics over various classes of frames, for example arbitrary, transitive, linear, and branching. It is remarkable that the satisfiability problem of the binder-free hybrid logic over arbitrary frames is decidable in PSPACE, which is the same as the complexity of deciding satisfiability in ordinary modal logic. Thus, hybridizing ordinary modal logic gives more expressive power, but the complexity stays the same. Some work has been carried out on simulating nominals inside modal logic, see Kracht and Wolter (1997).

It is remarkable that first-order hybrid logic offers precisely the features needed to prove interpolation theorems: While interpolation fails in a number of well-known first-order modal logics, their hybridized counterparts have this property, see Areces, Blackburn, and Marx (2003) as well as Blackburn and Marx (2003). The first paper gives a model-theoretic proof of interpolation whereas the second paper gives an algorithm for calculating interpolants based on a tableau system.

It should also be mentioned that logics similar to hybrid logics play a central role within the area of description logic, which is a family of logics used for knowledge representation in Artificial Intelligence, see the paper Blackburn and Tzakova (1998) and Carlos Areces' PhD thesis (2000).

## 6. Proof methods for hybrid logic

A number of papers have dealt with axioms for hybrid logic, for
example Blackburn (1993) and Blackburn and Tzakova (1999). The latter
paper gives an axiom system for hybrid logic and shows the remarkable
result that if the axiom system is extended with a set of additional
axioms which are *pure* formulas (that is, formulas where all
propositional symbols are nominals), then the extended axiom system is
complete with respect to the class of frames validating the axioms in
question. Pure formulas correspond to first-order conditions on the
accessibility relation (cf. the translation ST* _{a}*
above), so axiom systems for new hybrid logics with first-order
conditions on the accessibility relation can be obtained in a uniform
way simply by adding axioms as appropriate. So, if for example the
formula ↓

*c*□¬

*c*is added as an axiom, then the resulting system is complete with respect to irreflexive frames, cf. earlier. The paper Blackburn and ten Cate (2006) investigates

*orthodox*proof-rules (which are proof-rules without side-conditions) in axiom systems, and it is shown that if one requires extended completeness using pure formulas, then unorthodox proof-rules are indispensable in axiom systems for binder-free hybrid logic, but an axiom system can be given only involving orthodox proof-rules for the stronger hybrid logic including the ↓ binder. See also the paper Braüner (2006) (and the book Braüner (2011)) which gives another axiom system for hybrid logic as well as axiom systems for intuitionistic and paraconsistent hybrid logic.

Tableau, Gentzen, and natural deduction style proof-theory for hybrid logic work very well compared to ordinary modal logic. Usually, when a modal tableau, Gentzen, or natural deduction system is given, it is for one particular modal logic and it has turned out to be problematic to formulate such systems for modal logics in a uniform way without introducing metalinguistic machinery. This can be remedied by hybridization, that is, hybridization of modal logics enables the formulation of uniform tableau, Gentzen, and natural deduction systems for wide classes of logics. The paper Blackburn (2000) introduces a tableau system for hybrid logic that has this desirable feature: Analogous to the axiom system of Blackburn and Tzakova (1999), completeness is preserved if the tableau system is extended with a set of pure axioms, that is, a set of pure formulas that are allowed to be added to a tableau during the tableau construction. The tableau system of Blackburn (2000) is the basis for a decision procedure for the binder-free fragment of hybrid logic given in Bolander and Braüner (2006). This line of work has been continued in the papers Bolander and Blackburn (2007) and Bolander and Blackburn (2009). The paper Cerrito and Cialdea (2010) presents another tableau-based decision procedure for hybrid logic. Other decision procedures for hybrid logics, which also are based on proof-theory, are given in the paper Kaminski and Smolka (2009). The procedures of the latter paper are based on a higher-order formulation of hybrid logic involving the simply typed lambda calculus.

The paper Hansen, Bolander, and Braüner (2008) gives a tableau-based decision procedure for many-valued hybrid logic, that is, hybrid logic where the two-valued classical logic basis has been generalized to a many-valued logic basis involving a truth-value space having the structure of a finite Heyting algebra. Hansen (2010) gives a tableau-based decision procedure for a hybridized version of a dynamic epistemic logic called public annoucement logic. This is also a major issue of the forthcoming PhD thesis Hansen (2011).

Natural deduction style proof-theory of hybrid logic has been explored
in the papers Braüner (2004a), Braüner (2004b), Braüner
(2005a), and Braüner (2005b). The paper Braüner (2004a) also
gives a Gentzen system for hybrid logic. These natural deduction and
Gentzen systems can be extended with additional proof-rules
corresponding to first-order conditions on the accessibility relations
expressed by so-called *geometric theories* (this is of course
analogous to extending tableau and axiom systems with pure
axioms). See also Braüner and de Paiva (2006) where a natural
deduction system is given for intuitionistic hybrid logic. In the
context of situation theory, Gentzen and natural deduction systems for
logics similar to hybrid logics were explored already in the early
1990s by Jerry Seligman, see the overview in Seligman (2001). See the
book Braüner (2011) for a detailed treatment of hybrid-logical
proof-theory.

Work in resolution calculi and model checking is in the early phases, see Areces, de Rijke, and de Nivelle (2001) for resolution calculi and see as Franceschet and de Rijke (2006) as well as Lange (2009) for results on model checking.

Since the mid 1990s, the work on hybrid logic has flourished. For a detailed overview, see the handbook chapter Areces and ten Cate (2006). We refer the reader to the publications in the bibliography for further references. Moreover, see the internet resources below.

## Bibliography

- Areces, C., 2000.
*Logic Engineering. The Case of Description and Hybrid Logics*, Ph.D. thesis, Institute for Logic, Language and Computation, University of Amsterdam. - Areces C., Blackburn, P., and Marx, M., 1999. “The Computational
Complexity of Hybrid Temporal Logics”,
*The Logic Journal of the IGPL*, 8: 653–679. - –––, 2001. “Hybrid Logics: Characterization,
Interpolation and Complexity”,
*Journal of Symbolic Logic*, 66: 977–1010. - –––, 2003. “Repairing the Interpolation Theorem
in Quantified Modal Logic”,
*Annals of Pure and Applied Logic*, 124: 287–299. - Areces, C., de Rijke, M., and de Nivelle, H., 2001. “Resolution
in Modal, Description and Hybrid Logic”,
*Journal of Logic and Computation*, 11: 717–736. - Areces, C. and ten Cate, B., 2006. “Hybrid Logics”, in Blackburn, van Benthem, and Wolter (eds.) (2006).
- Blackburn, P., 1993. “Nominal Tense Logic”,
*Notre Dame Journal of Formal Logic*, 14: 56–83. - –––, 2000. “Internalizing Labelled
Deduction”,
*Journal of Logic and Computation*, 10: 137–168. - –––, 2007. “Arthur Prior and Hybrid
Logic”,
*Synthese*, 150: 329–372. - Blackburn, P. and Marx, M., 2003. “Constructive Interpolation in
Hybrid Logic”,
*Journal of Symbolic Logic*, 68: 463–480. - Blackburn, P. and ten Cate, B., 2006. “Pure Extensions, Proof
Rules, and Hybrid Axiomatics”,
*Studia Logica*, 84: 277–322. - Blackburn, P., van Benthem, J., and Wolter, F. (eds.),
2006.
*Handbook of Modal logic*, Amsterdam: Elsevier. - Blackburn, P. and Tzakova, M., 1998. “Hybridizing Concept
Languages”,
*Annals of Mathematics and Artificial Intelligence*, 24: 23–49. - –––, 1999. “Hybrid Languages and Temporal
Logic”,
*Logic Journal of the IGPL*, 7: 27–54. - Bolander, T. and Blackburn, P., 2007. “Termination for Hybrid
Tableaus”,
*Journal of Logic and Computation*, 17: 517–554. - –––, 2009. “Terminating Tableau Calculi
for Hybrid Logics Extending K”, in
*Proceedings of Methods for Modalities 5*(Electronic Notes in Theoretical Computer Science: Volume 231), pp. 21–39. - Bolander, T. and Braüner, T., 2006. “Tableau-Based Decision
procedures for Hybrid Logic”,
*Journal of Logic and Computation*, 16: 737–763. - Braüner, T., 2002. “Modal logic, Truth, and the Master
Modality”,
*Journal of Philosophical Logic*, 31: 359–386. - –––, 2004a. “Natural Deduction for Hybrid
Logic”,
*Journal of Logic and Computation*, 14: 329–353. - –––, 2004b. “Two Natural Deduction Systems for
Hybrid Logic: A Comparison”,
*Journal of Logic, Language, and Information*, 13: 1–23. - –––, 2005a. “Natural Deduction for First-Order
Hybrid Logic”,
*Journal of Logic, Language and Information*, 14: 173–198. - –––, 2005b. “Proof-Theoretic Functional
Completeness for the Hybrid Logics of Everywhere and
Elsewhere”,
*Studia Logica*, 81: 191–226. - –––, 2006. “Axioms for Classical,
Intuitionistic, and Paraconsistent Hybrid Logic”,
*Journal of Logic, Language, and Information*, 15: 179–194. - –––, 2011.
*Hybrid Logic and its Proof-Theory*(Applied Logic Series: Volume 37), Dordrecht-Heidelberg-Berlin-New York: Springer. - Braüner, T. and de Paiva, V., 2006. “Intuitionistic Hybrid
Logic”,
*Journal of Applied Logic*, 4: 231–255. - Bull, R., 1970. “An Approach to Tense Logic”,
*Theoria*, 36: 282–300. - Cerrito, S. and Cialdea, M., 2010. “Nominal Substitution at
Work with the Global and Converse Modalities”, in
*Advances in Modal Logic*(Volume 8), pp. 57–74. College Publications. - Copeland, J. (ed.), 1996.
*Logic and Reality: Essays in the Legacy of Arthur Prior*, Oxford: Clarendon Press. - Franceschet, M. and de Rijke, M., 2006. “Model Checking Hybrid
Logics (With An Application to Semistructured Data)”,
*Journal of Applied Logic*, 4: 279–304. - Gabbay, D. and Woods, J. (eds.), 2006.
*Logic and the Modalities in the Twentieth Century. The Handbook of the History of Logic*(Volume 7). Amsterdam: Elsevier. - Goranko, V., 1994. “Temporal Logic with Reference Pointers”, in
*Proceedings of the 1st International Conference on Temporal Logic*(Lecture Notes in Artificial Intelligence: Volume 827), pp. 133–148. Berlin: Springer. - Goranko, V., 1996. “Hierarchies of Modal and Temporal Logics with
Reference Pointers”,
*Journal of Logic, Language, and Information*, 5: 1–24. - Kaminski, M. and Smolka, G., 2009. “Terminating Tableau
Systems for Hybrid Logic with Difference and
Converse”,
*Journal of Logic, Language and Information*, 18: 437–464. - Kracht, M. and Wolter, F., 1997. “Simulation and Transfer Results
in Modal Logic — A Survey”,
*Studia Logica*, 59: 149–177. - Hansen, J.U., Bolander, T., and Braüner, T.,
2008. “Many-Valued Hybrid Logic”, in
*Advances in Modal Logic*(Volume 7), pp. 111–132. College Publications. - Hansen, J.U., 2010. “Terminating Tableaux for Dynamic
Epistemic Logics”, in
*Proceedings of the 6th Workshop on Methods for Modalities (M4M-6 2009)*(Electronic Notes in Theoretical Computer Science: Volume 262), pp. 141–156. - –––, 2011.
*A Logic Toolbox for Modeling Knowledge and Information in Multi-Agent Systems and Social Epistemology*, Ph.D. thesis, Roskilde University. Forthcoming. - Lange, M., 2009. “Model Checking for Hybrid
Logic”,
*Journal of Logic, Language and Information*, 18: 465–491. - Müller, T., 2007. “Prior's tense-logical
universalism”,
*Logique et Analyse*, 50: 223–252. - Øhrstrøm, P. and Hasle, P.,
1993. “A.N. Prior's Rediscovery of Tense
Logic”,
*Erkenntnis*, 39: 23–50. - –––, 2006. “A.N. Prior's Logic”, in Gabbay and Woods (2006), pp. 399–446.
- Passy, S. and Tinchev, T., 1985. “Quantifiers in Combinatory PDL:
Completeness, Definability, Incompleteness”, in
*Fundamentals of Computation Theory FCT 85*(Lecture Notes in Computer Science: Volume 199), pp. 512–519. Berlin: Springer. - Passy, S. and Tinchev, T., 1991. “An Essay in Combinatory Dynamic
Logic”,
*Information and Computation*, 93: 263–332. - Prior, A.N., 1967.
*Past, Present and Future*, Oxford: Clarendon Press. - –––, 1968.
*Papers on Time and Tense*, Oxford: Clarendon Press. - –––, 2003.
*Papers on Time and Tense*, Oxford: Oxford University Press. Second revised and expanded edition of Prior (1968). Edited by P. Hasle, P. Øhrstrøm, T. Braüner, and J. Copeland. - Prior, A.N. and Fine, K., 1977.
*Worlds, Times and Selves*, London: Duckworth. Based on manuscripts by Prior with a preface and a postscript by K. Fine. - Seligman, J., 2001. “Internalisation: The Case of Hybrid Logics”,
*Journal of Logic and Computation*, 11: 671–689. - Sylvan, R., 1996. “Other Withered Stumps of Time”, in Copeland (1996), pp. 111–130.
- ten Cate, B., 2004.
*Model Theory for Extended Modal Languages*, Ph.D. thesis, Institute for Logic, Language and Computation, University of Amsterdam.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.