hide
Free keywords:
-
Abstract:
Hybridization is a method invented by Arthur Prior for extending the
expressive power of modal languages. Although developed in
interesting ways by Robert Bull, and by the Sofia school (notably,
George Gargov, Valentin Goranko, Solomon Passy and Tinko Tinchev), the
method remains little known. In our view this has deprived temporal
logic of a valuable tool.
The aim of the paper is to explain why hybridization is useful in
temporal logic. We make two major points, the first technical, the
second conceptual. First, we show that hybridization gives rise to
well-behaved logics that exhibit an interesting synergy between modal
and classical ideas. This synergy, obvious for hybrid languages with
full first-order expressive strength, is demonstrated for a weaker
local language capable of defining the {\it Until\/} operator; we
provide a minimal axiomatization, and show that in a wide range of
temporally interesting cases extended completeness results can be
obtained automatically. Second, we argue that the idea of sorted
atomic symbols which underpins the hybrid enterprise can be developed
further. To illustrate this, we discuss the advantages and
disadvantages of a simple hybrid language which can quantify over
paths.
