P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....by ( R] 3. f i : R] jg, f j (i p)g, fi : pg by ( 4. f j ig, f j pg, f i :pg by (PARAM) 5. f i pg, f i :pg by (RES) 6. fg. Of course, we cannot expect a heuristic ensuring termination of our calculus for H( #) as the satis ability problem for H(#) is already undecidable (see [11]) 6 Conclusions Blackburn [10] argues that hybrid languages can be used to internalize labeled deduction. Similar ideas play a fundamental role in the labeled resolution systems we introduced in this paper. Once again, nominals labels together with the satis ability operator : or are the key ....

P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic.

....:pg by ( R] 3. f i : R] jg, f j (i p)g, fi : pg by ( 4. f j ig, f j pg, f i :pg by (PARAM) 5. f i pg, f i :pg by (RES) 6. fg. Of course, we cannot expect a heuristic ensuring termination of our calculus for H( #) as the satis ability problem for H(#) is already undecidable (see [11]) 6 Conclusions Blackburn [10] argues that hybrid languages can be used to internalize labeled deduction. Similar ideas play a fundamental role in the labeled resolution systems we introduced in this paper. Once again, nominals labels together with the satis ability operator : or are the key ....

P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic.

....in the 1990s it was realized that binding did not have to mean classical binding with 8 and 9, and the # binder was isolated. For early papers in this phase, see [22, 11] 7 For the Paste rule, which permits Henkin methods to be used in the basic hybrid language, see [16] For early work on # see [24, 15], and for the current state of play see [5] Hybrid proof theory, from a variety of perspectives, has blossomed in recent years, and we draw the readers attention to [38, 41, 18, 19, 12] For interpolation results see [5] and for computational complexity, see [4] That pretty much concludes the ....

P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic.

....However because G and H are interrelated the results of the previous section are not applicable. And in fact, adding even one nominal to tense logic causes a jump in complexity from pspace to exptime, and we don t need to add to obtain this result. Our proof uses the spy point technique from [BS95]; we will be exploring this technique in great detail in the following section when we discuss undecidable systems. Theorem 2. The K satisfaction problem for a language of tense logic containing at least one nominal is exptime hard. Proof. We shall reduce the exptime complete global ....

.... ) based interval logic in which quanti cation over t is permitted (see [All84] But because they o er full rst order expressivity over states, such hybrid languages are obviously undecidable. More recently, there has been interest in hybrid languages which use a weaker binder called # (see [Gor96,BS95]) Unlike 9 and 8, this is not a quanti er: it is simply a device which binds a nominal to the state where evaluation is being performed (that is, the current state) For example, the interplay between # and allows us to de ne the Until operator: Until( #x:3 #y: x (3(y ) 2(3y ....

[Article contains additional citation context not shown here]

P. Blackburn and J. Seligman. Hybrid languages. J. of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rstorder logic.

....#x: smooth talker 8y(htalks toiy : y htrustsix) Note the way the y switches the perspective from the node x (the politician) to his audience. I won t give a precise de nition of the syntax and semantics of hybrid languages with 8 and 9 here (you can nd all this in Blackburn and Seligman [15, 16] or Blackburn and Tzakova [18, 19] The previous examples tell you pretty much everything you need to know, and the discussion that follows should clarify things further. Remark 6.2 (We now have rst order expressivity) Our new hybrid logic is strong enough to express any rst order concept. ....

....rst order power, we don t have to. For a start, the use of in the hybrid translation is crucial . If we work with the free sublanguage, binding nominals to states with 9 and 8 does not yield full rstorder expressive power; for a counterexample, see Proposition 4. 5 of Blackburn and Seligman [15]. Hybrid logic decomposes the action of the classical quanti ers into two subtasks: perspective shifting (performed by ) and binding (performed by the hybrid binders 9 and 8) Moreover, we ve seen that there is a useful restricted form of these binders, namely #. Some recent papers have explored ....

[Article contains additional citation context not shown here]

P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic. 364 A Hybrid Logic Manifesto

....for H(#; from Theorem 4.4. Theorem 4.12 H(#; has the Beth de nability property. A careful analysis of weaker versions of the Beth property can be carried out for fragments of H(#; as we did with the interpolation property. 5 Complexity H(#; is undecidable (this is known from [BS95] unpublished work by Valentin Goranko, and can be proved directly for the bounded fragment [Woo81] but the sublanguage H( is decidable (this is an easy consequence of results in [PT91, GG93, Bla93] In this section we examine the computational complexity of H( and related systems, and ....

....of tense logic is pspace complete. However expanding such a language with even a single nominal (or free variable) results in an exptime hard satis ability problem. This happens even if we don t add all that s needed is one nominal. We prove this using the spypoint technique introduced in [BS95] We will use a more sophisticated version of this technique later in the paper to sharpen the undecidability result for H(#; Theorem 5.2 The K satis ability problem for a language of tense logic containing at least one nominal is exptime hard. Proof. We shall reduce the exptime complete ....

P. Blackburn and J. Seligman. Hybrid languages. Journal of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic.

....from the claim. So far, so good: nothing strange happens when we add transitivity to the basic hybrid language. But as we will now show, transitivity is not enough to tame hybridization when the backward looking modality P is added. The proof that follows uses the spypoint technique from [BS95, ABM99] Theorem 3.4 The satis ability problem over transitive frames for the Priorean tense language expanded with just one nominal (and no operator) is exptime hard. Proof. We will reduce the exptime complete global K satis ability problem for unimodal languages to the (local) satis ....

P. Blackburn and J. Seligman. Hybrid languages. J. of Logic, Language and Information, 4(3):251-272, 1995. Special issue on decompositions of rst-order logic.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.