A decidable temporal logic with repeating values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this paper, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets. This is a surprising result since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier.

Temporal Logics of Repeating Values

Various logical formalisms with the freeze quantifier have been recently considered to model computer systems even though this is a powerful mechanism that often leads to undecidability. In this article, we study a linear-time temporal logic with past-time operators such that the freeze operator is only used to express that some value from an infinite set is repeated in the future or in the past. Such a restriction has been inspired by a recent work on spatio-temporal logics that suggests such a restricted use of the freeze operator. We show decidability of finitary and infinitary satisfiability by reduction into the verification of temporal properties in Petri nets by proposing a symbolic representation of models. This is a quite surprising result in view of the expressive power of the logic since the logic is closed under negation, contains future-time and past-time temporal operators and can express the nonce property and its negation. These ingredients are known to lead to undecidability with a more liberal use of the freeze quantifier. The article also contains developments about the relationships between temporal logics with the freeze operator and counter automata as well as reductions into first-order logics over data words.

Las ideas lingüísticas de Juan Mateo Zabala: El verbo regular vascongado del dialecto vizcaíno (1848)

Presentado en las II. Jornadas de Lingüística Vasco-Románica / Euskal-Erromantze Linguistika II. Jardunaldietan aurkeztua (Bilbo, 2007)

Erronkarierazko dotrina argitaragabe bat: edizioa eta azterketa

[EU] Gure diputazioetako artxiboetan gordetzen diren eskuizkribu anitzetarik bat ematen dut lan honetan argitara: Nafarroako Artxibo Nagusiko Bonaparte Ondarean B-118 signatura daraman "Doctrina Uscaraz", erronkarieraz idatzitako dotrina osatugabea. Testu honen edizioa paratzeaz gain, iruzkina ere eransten dut, hala testuko puntu ilunak hobeki ulertarazteko nola kontu askotan hain bitxi gertatzen zaigun erronkariera ezagutzeko aurrerapauso txiki bat egiteko asmoz.

Clonación, expresión y purificación de la proteína estructural VP4 de la cápside del Virus del triatoma (TrV; Dicistroviridae: Cripaviridae)

Triatoma virus (TrV) es un virus patógeno de Triatoma infestans y otros insectos hematófagos , que son los vectores principales de la enfermedad del Chagas (tripanosomiasis americana) . Esta enfermedad es un grave problema sanitario en muchos países de Latinoamérica , do nde es endé mic a y afecta alrededor de 8 millones de personas. El agente causante de dicha enfermedad es el protozoo parásito Tripanosoma cruzi , que infecta al insecto vector y este a su vez , infecta hospedadores vertebrados cuando se alimenta de su sangre [Rassi et al ., 2010] . Al aumentar el movimiento migracional de las personas , la enfermedad ha logrado exte nde rse a otras regiones y convertirse en un problema de salud en z o nas originariamen te no endémicas [ Gascon et a l ., 2010 ] . Debido a esto se ha propuesto el uso de TrV como agente de control biológico frente a los vectores de la enfermedad del Chagas

XVIII. mendeko aditz taula batzuk: Joanes Erauskinen eskuizkribua

Beatriz Fernández & Pello Salaburu (arg. / eds.)

O vocativo nem no imaginário linguístico brasileiro

Este estudo tem por objetivo analisar o vocativo nem, oriundo do dialeto social da cidade do Rio de Janeiro, no imaginário linguístico brasileiro, a partir do conceito de Patrick Charaudeau (2008) sobre o imaginário sociodiscursivo. A perspectiva teórica abordada está centrada na Análise do Discurso. Apresenta-se, no início, o referencial teórico que embasou o estudo e, posteriormente, descreve-se o percurso da pesquisa, que contempla o corpus colhido em redes sociais de relacionamento e blogs. Além do material encontrado para a pesquisa, também foram aproveitadas algumas experiências pessoais sobre o tema, tanto em sala de aula, quanto em conversas com amigos. Durante a pesquisa, buscou-se realizar a descrição do vocábulo, a partir de breves comentários a respeito da variação linguística e preconceito linguístico, bem como sobre atitudes, crenças e imaginários. A análise conduzida demonstrou os tipos de crença negativa que circulam em determinado grupo social, bem como a construção da identidade, de alguns indivíduos das classes consideradas desprestigiadas socialmente, que pode ser percebida por determinadas atitudes dos falantes. Há algum tempo, não era observada nos falantes uma afirmação da identidade. Esse comportamento recente só pode ser analisado dessa forma, visto que este estudo aconteceu quase que em tempo real. Como resultado, a pesquisa revelou o imaginário negativo que os falantes da variedade prestigiosa da língua cultivam em relação aos usos, e aos usuários, do referido item lexical. Da mesma forma, foi observado como os usuários do vocativo se posicionavam frente à rejeição. Tais reflexões podem colaborar para os estudos linguísticos de forma a minimizar o preconceito linguístico no ensino da língua materna em relação à variedade que faz parte do dialeto desprestigiado socialmente

Ondarroako haurren jariotasuna eta lexikoaren azterketa

[eus] Jakina da eskolan arrakasta izateko hizkuntzaren erabilera aldagai garrantzitsua dela. Hori horrela, lan honetan 4-7 urte bitarteko hamabi neska mutilen jariotasuna eta lexikoaren ezagutza aztertzen dira. Betiere, kontuan izanda haur horien ama hizkuntza ezberdina dela, hots, euskara edota erdara (atzerriko edozein hizkuntza). Helburua herriko hizkera lagunartean (eskolan) bertan gauzatzen dela frogatzea da. Horretarako, haur hauek galdetegi baten bidez elkarrizketatu dira. Jarraian transkribatu eta honen azterketa linguistikoa egin da, jariotasuna eta lexiko aztertuz. Azkenik, konparaketa taulez baliatuz galdetegietako emaitzak aztertu dira eta zenbait haurrek hitz egiterako orduan erakusten duten jariotasuna handitu ahal izateko eskolan lantzeko zenbait proposamen egin dira.

Bizkaiko jauntxoen inguruko herri literaturaz: Plentziako 1603ko hiru esaera zahar eta "Refranes y Sentencias"-en jatorria, eta proposamen bat Arrasateko erreketaren kantuez

[EUS] Lan honetan aurkikuntza baten berri ematen dugu: Plentziako armarri batean aurkitutako hiru euskal esaera zahar (1603) aurkezten eta hizkuntzaren eta historiaren ikuspuntutik aztertzen ditugu. Hiru esaerotatik bi «Refranes y sentencias» 1596) lanean agertzen dira, eta hori datu garrantzitsua da; izan ere, Lakarrak 1996) errefrau-bilduma anonimo horren jatorriaz egindako proposamena berresteko argudio berria da. Zehazki, Bizkaiko ipar-mendebala proposatu zuen Lakarrak bildumako errefrauen jatorri gisa. Beste alde batetik, Bizkaiko ipar-mendebaleko euskararen zenbait ezaugarri baliatuta, Arrasateko erreketari buruzko zenbait kantu eremu horretan sortu zirela proposatzen dugu —zehazki, Butroeko (Gatika) dorretxearen inguruan—, hizkuntzari dagozkion argudioak historiari buruzkoekin osatuta.

Joanes Erauskinen aditz taulak: azterketa gramatikografiko eta linguistikoa

Gotzon Aurrekoetxea, Jesus Mari Makazaga & Patxi Salaberri Muñoa (eds.)

Graphone model interpolation and Arabic pronunciation generation

This paper extends n-gram graphone model pronunciation generation to use a mixture of such models. This technique is useful when pronunciation data is for a specific variant (or set of variants) of a language, such as for a dialect, and only a small amount of pronunciation dictionary training data for that specific variant is available. The performance of the interpolated n-gram graphone model is evaluated on Arabic phonetic pronunciation generation for words that can't be handled by the Buckwalter Morphological Analyser. The pronunciations produced are also used to train an Arabic broadcast audio speech recognition system. In both cases the interpolated graphone model leads to improved performance. Copyright © 2011 ISCA.

Tandem system adaptation using multiple linear feature transforms

Adaptation to speaker and environment changes is an essential part of current automatic speech recognition (ASR) systems. In recent years the use of multi-layer percpetrons (MLPs) has become increasingly common in ASR systems. A standard approach to handling speaker differences when using MLPs is to apply a global speaker-specific constrained MLLR (CMLLR) transform to the features prior to training or using the MLP. This paper considers the situation when there are both speaker and channel, communication link, differences in the data. A more powerful transform, front-end CMLLR (FE-CMLLR), is applied to the inputs to the MLP to represent the channel differences. Though global, these FE-CMLLR transforms vary from time-instance to time-instance. Experiments on a channel distorted dialect Arabic conversational speech recognition task indicates the usefulness of adapting MLP features using both CMLLR and FE-CMLLR transforms. © 2013 IEEE.

~(126)Cs的高自旋态能级结构

利用融合蒸发反应 116Cd(14 N ,4n) 12 6Cs布居了 12 6Cs的高自旋态 .观测到了 10 0多条新的γ跃迁和相应的能级 ,建立了双奇核 12 6Cs由 9个转动带构成的能级纲图 .尝试性地指定了大部分能级的自旋和宇称以及各转动带的Nilsson单粒子组态 .极大地丰富了已有的实验结果 .

RABBIT: A Compiler for SCHEME

We have developed a compiler for the lexically-scoped dialect of LISP known as SCHEME. The compiler knows relatively little about specific data manipulation primitives such as arithmetic operators, but concentrates on general issues of environment and control. Rather than having specialized knowledge about a large variety of control and environment constructs, the compiler handles only a small basis set which reflects the semantics of lambda-calculus. All of the traditional imperative constructs, such as sequencing, assignment, looping, GOTO, as well as many standard LISP constructs such as AND, OR, and COND, are expressed in macros in terms of the applicative basis set. A small number of optimization techniques, coupled with the treatment of function calls as GOTO statements, serve to produce code as good as that produced by more traditional compilers. The macro approach enables speedy implementation of new constructs as desired without sacrificing efficiency in the generated code. A fair amount of analysis is devoted to determining whether environments may be stack-allocated or must be heap-allocated. Heap-allocated environments are necessary in general because SCHEME (unlike Algol 60 and Algol 68, for example) allows procedures with free lexically scoped variables to be returned as the values of other procedures; the Algol stack-allocation environment strategy does not suffice. The methods used here indicate that a heap-allocating generalization of the "display" technique leads to an efficient implementation of such "upward funargs". Moreover, compile-time optimization and analysis can eliminate many "funargs" entirely, and so far fewer environment structures need be allocated at run time than might be expected. A subset of SCHEME (rather than triples, for example) serves as the representation intermediate between the optimized SCHEME code and the final output code; code is expressed in this subset in the so-called continuation-passing style. As a subset of SCHEME, it enjoys the same theoretical properties; one could even apply the same optimizer used on the input code to the intermediate code. However, the subset is so chosen that all temporary quantities are made manifest as variables, and no control stack is needed to evaluate it. As a result, this apparently applicative representation admits an imperative interpretation which permits easy transcription to final imperative machine code. These qualities suggest that an applicative language like SCHEME is a better candidate for an UNCOL than the more imperative candidates proposed to date.

Staging Swissness : Inter-and Intracultural Theatre Translation

Wilkinson, Jane, 'Staging Swissness: Inter- and Intracultural Theatre Translation', Language and Intercultural Communication (2005) 5(1) pp.72-85 RAE2008