% % GENERATED FROM https://www.coli.uni-saarland.de % by : anonymous % IP : coli2006.lst.uni-saarland.de % at : Mon, 05 Feb 2024 15:43:07 +0100 GMT % % Selection : Author: Patrick_Blackburn % @TechReport{Areces_et_al:1999, AUTHOR = {Areces, Carlos and Blackburn, Patrick and Marx, Maarten}, TITLE = {Hybrid Logics: Characterization, Interpolation and Complexity}, YEAR = {1999}, MONTH = {February}, NUMBER = {108}, PAGES = {35}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus108.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus108.dvi}, ABSTRACT = {Hybrid languages are extended modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least 1967 (in the work of Arthur Prior), but recent work has focussed on more constrained systems. The purpose of the present paper is to examine one such system in detail. We begin by studying its expressivity, and provide both model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraisse game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that the system corresponds precisely to the first-order fragment which is invariant for generated submodels. We further establish that it has (strong) interpolation, and provide failure results in the finite variable fragments. We also show that weak interpolation holds for an important sublanguage and provide complexity results for this sublanguage and other fragments and variants (the full logic being undecidable).}, ANNOTE = {COLIURL : Areces:1999:HLC.pdf Areces:1999:HLC.ps Areces:1999:HLC.dvi} } @TechReport{Blackburn:1998, AUTHOR = {Blackburn, Patrick}, TITLE = {Internalizing Labeled Deduction}, YEAR = {1998}, MONTH = {November}, NUMBER = {102}, PAGES = {39}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus102.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus102.dvi}, ABSTRACT = {This paper shows how to internalize the Kripke satisfaction definition using labeled modal languages and explores the proof theoretic consequences of this. As we shall see, using labeled modal languages enables us to transfer classic Gabbay-style labeled deduction from the metalanguage to the object language, and to handle the required labeling discipline purely logically. Moreover, internalized labeled deduction links neatly with the Gabbay-style rules now widely used in modal Hilbert-systems, completeness results for a wide range of first-order definable frame classes can be obtained automatically, and the method extends straightforwardly to richer languages. The paper discusses related work by Jerry Seligman and Miroslava Tzakova and concludes with some reflections on the status of labeling in modal logic.}, ANNOTE = {COLIURL : Blackburn:1998:ILD.pdf Blackburn:1998:ILD.ps Blackburn:1998:ILD.dvi} } @TechReport{Blackburn_Bos:1997, AUTHOR = {Blackburn, Patrick and Bos, Johan}, TITLE = {Representation and Inference for Natural language. A First Course in Computational Semantics}, YEAR = {1997}, MONTH = {August}, NUMBER = {90}, PAGES = {50}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS Report}, INSTITUTION = {Universität des Saarlandes}, URL = {http://www.iccs.informatics.ed.ac.uk/~jbos/comsem/download/volume1.ps.gz}, ABSTRACT = {These are the course notes for Representation and Inference for Natural Language: A First Course in Computational Semantics, which will be given in the second week of ESSLLI97, Aix-en-Provence, by Patrick Blackburn and Johan Bos. The course is an introduction to computational semantics in Prolog. It introduces some fundamental techniques for computing semantic representations for natural language, and working with the result. Both the underlying theory, and their implementation in Prolog, are discussed. We believe that the reader who masters these techniques will be in a good position to appreciate (and critically assess) ongoing developments in computational semantics.}, ANNOTE = {COLIURL : Blackburn:1997:RIN.pdf Blackburn:1997:RIN.ps} } @TechReport{Blackburn_et_al:1998, AUTHOR = {Blackburn, Patrick and Bos, Johan and Kohlhase, Michael and de Nivelle, Hans}, TITLE = {Inference and Computational Semantics}, YEAR = {1998}, MONTH = {November}, NUMBER = {106}, PAGES = {15}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus106.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus106.dvi}, ABSTRACT = {This paper discusses inference in computational semantics. We argue that state-of-the-art methods in first-order it theorem proving/ and it model building/ are of direct relevance to inference for natural language processing. We support our claim by discussing our implementation of van der Sandt's presupposition projection algorithm in Discourse Representation Theory, an algorithm which demands sustained use of powerful inference mechanisms.}, ANNOTE = {COLIURL : Blackburn:1998:ICS.pdf Blackburn:1998:ICS.ps Blackburn:1998:ICS.dvi} } @InCollection{Blackburn_et_al:2001, AUTHOR = {Blackburn, Patrick and Bos, Johan and Kohlhase, Michael and de Nivelle, Hans}, TITLE = {Inference and Computational Semantics}, YEAR = {2001}, BOOKTITLE = {Computing Meaning}, VOLUME = {2}, NUMBER = {77}, PAGES = {11-28}, EDITOR = {Bunt, Harry and Muskens, Reinhard and Thijsse, Elias}, SERIES = {Studies in Linguistics and Philosophie}, ADDRESS = {Dordrecht}, PUBLISHER = {Kluwer Academic Publishers} } @TechReport{Blackburn_de Rijke:1994, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten}, TITLE = {Zooming In, Zooming Out}, YEAR = {1994}, MONTH = {November}, NUMBER = {48}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/claus/claus48.dvi ftp://ftp.coli.uni-sb.de/pub/claus/claus48.ps}, ABSTRACT = {This is an exploratory paper about combining logics, combining theories and combining structures. Typically when one applies logic to such areas as computer science, artificial intelligence or linguistics, one encounters hybrid ontologies. The aim of this paper is to identify plausible strategies for coping with ontological richness.}, ANNOTE = {COLIURL : Blackburn:1994:ZZ.pdf Blackburn:1994:ZZ.ps Blackburn:1994:ZZ.dvi} } @TechReport{Blackburn_de Rijke:1995, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten}, TITLE = {Why Combine Logics?}, YEAR = {1995}, MONTH = {April}, NUMBER = {57}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus57.ps}, ABSTRACT = {Combining logics has become a rapidly expanding enterprise that is inspired mainly by concerns about modularity and the wish to join together tailored made logical tools into more powerful but still manageable ones. A natural question is whether it offers anything new over and above existing standard languages. By analysing a number of applications where combined logics arise, we argue that combined logics are a potentially valuable tool in applied logic, and that endorsements of standard languages often miss the point. Using the history of quantified modal logic as our main example, we also show that the use of combined structures and logics is a recurring theme in the analysis of existing logical systems.}, ANNOTE = {COLIURL : Blackburn:1995:WCL.pdf Blackburn:1995:WCL.ps} } @Article{Blackburn_de Rijke:1996, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten}, TITLE = {Combining Logics. Special Issue}, YEAR = {1996}, JOURNAL = {Notre Dame Journal of Formal Logic}, VOLUME = {37} } @Article{Blackburn_de Rijke:1997, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten}, TITLE = {Why Combine Logics?}, YEAR = {1997}, JOURNAL = {Studia Logica. An International Journal for Symbolic Logic}, VOLUME = {59}, NUMBER = {1}, PAGES = {5-27}, NOTE = {but published later} } @Article{Blackburn_de Rijke:1997_1, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten}, TITLE = {Zooming In, Zooming Out}, YEAR = {1997}, JOURNAL = {Journal of Logic, Language and Information}, VOLUME = {6}, PAGES = {5-31} } @TechReport{Blackburn_et_al:1994, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten and Vennema, Ide}, TITLE = {The Algebra of Modal Logic}, YEAR = {1994}, MONTH = {November}, NUMBER = {47}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/claus/claus47.dvi}, ABSTRACT = {Our main aim is to review the frame semantics and axiomatics of modal logic from the perspective of the duality between (Kripke) frames and boolean algebras with operators as defined by Jónsson and Tarski. To this end, we introduce modal languages and their interpretation in models and frames in Part II. We define and discuss the notion of a modal formula characterizing a class of frames or models, and give the Sahlqvist algorithm which yields, given a suitable modal formula as input, the corresponding first-order condition on the class of frames characterized by the formula. We define the concept of a normal modal logic and explain the canonical frame method for proving completeness of a logic with respect to classes of frames. In Part III we develop the algebraic perspective on modal logic. We introduce boolean algebras with operators and show how they arise naturally in both the semantic and the axiomatic approach towards algebraizing modal logic. We discuss in detail how the category of boolean algebras with operators and homomorphisms links up with the category of frames with so-called bounded morphisms. Finally, we apply this duality to give easy proofs for some important and well-known results from modal logic.}, ANNOTE = {COLIURL : Blackburn:1994:AML.ps Blackburn:1994:AML.dvi} } @TechReport{Blackburn_et_al:1995, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten and Vennema, Ide}, TITLE = {Relational Methods in Logic, Language and Information}, YEAR = {1995}, MONTH = {September}, NUMBER = {65}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus65.ps}, ABSTRACT = {This paper discusses the use of relational methods in the interdisciplinary field of Logic, Language and Information. We first sketch the developments that lead to the current focus on dynamics in the area. After that we give examples of logics of transitions that naturally arise in this setting, and we identify more general themes such as bisimulations, relativisations and dynamic modes of inference. We conclude with a discussion of newly emerging themes, and the limitations of the relational perspective.}, ANNOTE = {COLIURL : Blackburn:1995:RML.pdf Blackburn:1995:RML.ps} } @InCollection{Blackburn_et_al:1997, AUTHOR = {Blackburn, Patrick and de Rijke, Maarten and Vennema, Ide}, TITLE = {Relational Methods in Logic, Language and Information}, YEAR = {1997}, BOOKTITLE = {Relational Methods in Computer Science}, PAGES = {211-225}, EDITOR = {Brink, C. and Kahl, W. and Schmidt, G.}, SERIES = {Advances in Computing Sciences}, ADDRESS = {Berlin}, PUBLISHER = {Springer} } @InProceedings{Blackburn_Gardent:1995, AUTHOR = {Blackburn, Patrick and Gardent, Claire}, TITLE = {A Specification Language for Lexical Functional Grammars}, YEAR = {1995}, BOOKTITLE = {7th Conference of the European Chapter of the Association for Computational Linguistics (EACL '91)}, PAGES = {39-44}, ADDRESS = {Dublin} } @TechReport{Blackburn_Gardent:1995_1, AUTHOR = {Blackburn, Patrick and Gardent, Claire}, TITLE = {A Specification Language for Lexical Functional Grammars}, YEAR = {1995}, MONTH = {February}, NUMBER = {51}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus51.ps ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus51.dvi}, ABSTRACT = {This paper defines a language L for specifying LFG grammars. This enables constraints on LFG's composite ontology (c-structures synchronised with f-structures) to be stated directly; no appeal to the LFG construction algorithm is needed. We use L to specify schemata annotated rules and the LFG uniqueness, completeness and coherence principles. Broader issues raised by this work are noted and discussed.}, ANNOTE = {COLIURL : Blackburn:1995:SLLb.pdf Blackburn:1995:SLLb.ps Blackburn:1995:SLLb.dvi} } @InProceedings{Blackburn_Gardent:1998, AUTHOR = {Blackburn, Patrick and Gardent, Claire}, TITLE = {A Description Language for Discourse Semantics}, YEAR = {1998}, BOOKTITLE = {Logical Aspects of Computational Linguistics (LACL '98), December 14-16}, ADDRESS = {Grenoble, France} } @TechReport{Blackburn_et_al:1996, AUTHOR = {Blackburn, Patrick and Jaspars, Jan and de Rijke, Maarten}, TITLE = {Reasoning about Changing Information}, YEAR = {1996}, MONTH = {September}, NUMBER = {81}, PAGES = {25}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus81.ps}, ABSTRACT = {The purpose of these notes is two-fold: (i) to give a reasonably self-contained introduction to a particular approach to theory change, known as the Alchourron-Gardenfors-Makinson (AGM) approach, and to discuss some of the alternatives and extensions that have been proposed to it over the past few years; (ii) to relate the AGM approach to other 'information-oriented' branches of logic, including intuitionistic logic, non-monotonic reasoning, verisimilitude, and modal and dynamic logic.}, ANNOTE = {COLIURL : Blackburn:1996:RAC.pdf Blackburn:1996:RAC.ps} } @TechReport{Blackburn_et_al:1995_1, AUTHOR = {Blackburn, Patrick and Meyer-Viol, Wilfried and de Rijke, Maarten}, TITLE = {A Proof System for Finite Trees}, YEAR = {1995}, MONTH = {October}, NUMBER = {67}, PAGES = {19}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus67.ps}, ABSTRACT = {In this paper we introduce a description language for finite trees. Although we briefly note some of its intended applications, the main goal of the paper is to provide it with a sound and complete proof system. We do so using standard axioms from modal provability logic and modal logics of programs, and prove completeness by extending techniques due to Van Benthem and Meyer-Viol and Blackburn and Meyer-Viol. We conclude with a proof of the EXPTIME-completeness of the satisfiability problem, and a discussion of issues related to complexity and theorem proving.}, ANNOTE = {COLIURL : Blackburn:1995:PSFb.pdf} } @InProceedings{Blackburn_et_al:1995_2, AUTHOR = {Blackburn, Patrick and Meyer-Viol, Wilfried and de Rijke, Maarten}, TITLE = {A Proof System for Finite Trees}, YEAR = {1995}, BOOKTITLE = {Computer Science Logic. 9th International Workshop (CSL '95)}, NUMBER = {1092}, PAGES = {86-105}, EDITOR = {Kleine Büning, H.}, SERIES = {Lecture Notes in Computer Science}, ADDRESS = {Berlin}, PUBLISHER = {Springer} } @TechReport{Blackburn_Seligman:1995, AUTHOR = {Blackburn, Patrick and Seligman, Jerry}, TITLE = {Hybrid Languages}, YEAR = {1995}, MONTH = {October}, NUMBER = {66}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {ftp://ftp.coli.uni-sb.de/pub/coli/claus/claus66.ps}, ABSTRACT = {Hybrid languages have both modal and first-order characteristics: a Kripke semantics, and explicit variable binding apparatus. This paper motivates the development of hybrid languages, sketches their history, and examines the expressive power of three hybrid binders. We show that all three binders give rise to languages strictly weaker than the corresponding first-order language, that full first-order expressivity can be gained by adding the universal modality, and that all three binders can force the existence of infinite models and have undecidable satisfiability problems.}, ANNOTE = {COLIURL : Blackburn:1995:HLA.pdf Blackburn:1995:HLA.ps} } @Article{Blackburn_Seligman:1995_1, AUTHOR = {Blackburn, Patrick and Seligman, Jerry}, TITLE = {Hybrid Languages}, YEAR = {1995}, JOURNAL = {Journal of Logic, Language and Information}, VOLUME = {4}, PAGES = {251-272} } @TechReport{Blackburn_Seligman:1996, AUTHOR = {Blackburn, Patrick and Seligman, Jerry}, TITLE = {What are Hybrid Languages?}, YEAR = {1996}, MONTH = {November}, NUMBER = {83}, PAGES = {19}, ADDRESS = {Saarbrücken}, TYPE = {CLAUS-Report}, INSTITUTION = {Universität des Saarlandes}, URL = {http://turing.wins.uva.nl/~carlos/hybrid/Papers/what.pdf}, ABSTRACT = {Hybrid languages exhibit two kinds of hybridisation. First, they combine the distinguishing features of modal logic and classical logic: although they have a Kripke semantics, they also make use of explicit variables and quantifiers that bind them. Second, they don't draw a syntactic distinction between terms and formulas: terms are part of the formula algebra, thus enabling the free combination of two different types of information. The goals of this paper are to introduce a number of hybrid languages, to discuss some of their fundamental logical properties (expressivity, decidability, and undecidability), and then, brie to indicate why such systems deserve further attention. Although hybrid languages have a long and varied history, it is quite likely that most readers will know little, if anything, about them. This dictates the structure of this paper: before we can explain why we're interested in hybrid languages, we're going to have to explain what they are and give some insight into their capabilities, for only then will a discussion of broader motivational issues make much sense.}, ANNOTE = {COLIURL : Blackburn:1996:WHL.pdf} } @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} } @InProceedings{Bos:2001, AUTHOR = {Bos, Johan}, TITLE = {DORIS 2001: Underspecification, Resolution and Inference for Discourse Representation Structures}, YEAR = {2001}, BOOKTITLE = {Proceedings of the Workshop on Inference in Compuational Semantics (ICoS-3), June 18-19}, EDITOR = {Blackburn, Patrick and Kohlhase, Michael}, ADDRESS = {Siena, Italy}, URL = {https://www.coli.uni-saarland.de/~bos/doris2001.pdf}, ANNOTE = {COLIURL : Bos:2001:DUR.pdf} } @InProceedings{Striegnitz:2001, AUTHOR = {Striegnitz, Kristina}, TITLE = {Model Checking for Contextual Reasoning in NLG}, YEAR = {2001}, BOOKTITLE = {Proceedings of Inference in Computational Semantics (ICoS-3), June 18-23}, PAGES = {101-115}, EDITOR = {Blackburn, Patrick and Kohlhase, Michael}, ADDRESS = {Siena, Italy}, URL = {https://www.coli.uni-saarland.de/cl/projects/indigen/papers/icos3.ps.gz}, ABSTRACT = {Presupposition triggers, such as e.g. 'the', 'too', 'another', impose constraints on the context they are used in. A violation of these constraints results in an infelicitous utterance. A natural language generation system therefore has to reason on the context to check that they are satisfied. We argue that this kind of contextual reasoning is essentially a model checking task and demonstrate this for a variety of presupposition triggers. To account for the influence of some background knowledge, we propose to embed queries to a description logic knowledge base in a first order model checking algorithm.}, ANNOTE = {COLIURL : Striegnitz:2001:MCC.pdf Striegnitz:2001:MCC.ps} }