%
% GENERATED FROM https://www.coli.uni-saarland.de
%    by   : anonymous
%    IP   : coli2006.lst.uni-saarland.de
%    at   : Mon, 05 Feb 2024 15:43:24 +0100 GMT
%    
% Selection : Author: Miroslava_Tzakova
%




@TechReport{Blackburn_Tzakova:1998,
      AUTHOR = {Blackburn, Patrick and Tzakova, Miroslava},
      TITLE = {Hybrid Completeness},
      YEAR = {1998},
      MONTH = {June},
      NUMBER = {95},
      PAGES = {27},
      ADDRESS = {Saarbrücken},
      TYPE = {CLAUS Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus95.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus95.dvi},
      ABSTRACT = {In this paper we discuss two hybrid languages, and provide them with complete axiomatizations. Both languages combine features of modal and classical logic. Like modal languages, they contain modal operators and have a Kripke semantics. Unlike modal languages, in these systems it is possible to 'label' states by using binders to bind special state variables. This paper explores the consequences of hybridization for completeness. As we shall show, the challenge is to blend the modal idea of canonical models with the classical idea of witnessed maximal consistent sets. The languages discussed provide us with two extreme examples of the issues involved. In the one case we can combine these ideas relatively straightforwardly with the aid of analogs of the Barcan axioms coupled with a modal theory of labeling. In the other case, although we can still formulate a theory of labeling, the Barcan analogs are not valid. We show how to overcome this difficulty by using COV, an infinite collection of additional rules of proof which has been used in a number of investigations of extended modal logic.},
      ANNOTE = {COLIURL : Blackburn:1998:HC.pdf Blackburn:1998:HC.ps Blackburn:1998:HC.dvi}
}

@TechReport{Blackburn_Tzakova:1998_1,
      AUTHOR = {Blackburn, Patrick and Tzakova, Miroslava},
      TITLE = {Hybrid Languages and Temporal Logic (Full Version)},
      YEAR = {1998},
      MONTH = {July},
      NUMBER = {96},
      PAGES = {50},
      ADDRESS = {Saarbrücken},
      TYPE = {CLAUS Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus96.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus96.dvi},
      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 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. Technically, 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 three weaker local languages, all of which are capable of defining the Until operator; we provide simple minimal axiomatizations for all three systems, and show that in a wide range of temporally interesting cases, extended completeness results can be obtained automatically. Conceptually, we argue that the idea of sorted atomic symbols which underpins the hybrid enterprise can be developed much further. To illustrate this, we discuss the advantages and disadvantages of a simple hybrid language which can quantify over paths. This is the original version of a paper which was accepted for publication in a special issue of the Journal of the IGPL on temporal logic. Unfortunately, the length of the article meant that it had to be drastically cut, and only a shorter version will appear. While the short version covers one of the most elegant results (@-driven completeness results) and is slightly more up to date in certain respects, the long version is probably the most detailed discussion of the completeness theory of local hybrid languages around. The long version also contains many lengthy footnotes. These outline the history of hybrid languages in considerable detail, and contain many remarks on philosophical, methodological, and technical issues.},
      ANNOTE = {COLIURL : Blackburn:1998:HLTa.pdf Blackburn:1998:HLTa.ps Blackburn:1998:HLTa.dvi}
}

@TechReport{Blackburn_Tzakova:1998_2,
      AUTHOR = {Blackburn, Patrick and Tzakova, Miroslava},
      TITLE = {Hybridizing Concept Languages},
      YEAR = {1998},
      MONTH = {October},
      NUMBER = {97},
      PAGES = {26},
      ADDRESS = {Saarbrücken},
      TYPE = {CLAUS-Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus97.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus97.dvi},
      ABSTRACT = {This paper shows how to increase the expressivity of concept languages using a strategy called hybridization. Building on the well-known correspondences between modal and description logics, two hybrid languages are defined. These languages are called 'hybrid' because, as well as the familiar propositional variables and modal operators, they also contain variables across individuals and a binder that binds these variables. As is shown, combining aspects of modal and first-order logic in this manner allows the expressivity of concept languages to be boosted in a natural way, making it possible to define number restrictions, collections of individuals, irreflexivity of roles, and TBox- and ABox-statements. Subsequent addition of the universal modality allows the notion of subsumption to internalized, and enables the representation of queries to arbitrary first-order knowledge bases. The paper notes themes shared by the hybrid and concept language literatures, and draws attention to a little-known body of work by the late Arthur Prior.},
      ANNOTE = {COLIURL : Blackburn:1998:HCL.pdf Blackburn:1998:HCL.ps Blackburn:1998:HCL.dvi}
}

@TechReport{Blackburn_Tzakova:1998_3,
      AUTHOR = {Blackburn, Patrick and Tzakova, Miroslava},
      TITLE = {Hybrid Languages and Temporal Logic},
      YEAR = {1998},
      MONTH = {November},
      NUMBER = {107},
      PAGES = {30},
      ADDRESS = {Saarbrücken},
      TYPE = {CLAUS Report},
      INSTITUTION = {Universität des Saarlandes},
      URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus107.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus107.dvi},
      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 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.},
      ANNOTE = {COLIURL : Blackburn:1998:HLTb.pdf Blackburn:1998:HLTb.ps}
}