Invariant-free deduction systems for temporal logic

In this thesis we propose a new approach to deduction methods for temporal logic. Our proposal is based on an inductive definition of eventualities that is different from the usual one. On the basis of this non-customary inductive definition for eventualities, we first provide dual systems of tableaux and sequents for Propositional Linear-time Temporal Logic (PLTL). Then, we adapt the deductive approach introduced by means of these dual tableau and sequent systems to the resolution framework and we present a clausal temporal resolution method for PLTL. Finally, we make use of this new clausal temporal resolution method for establishing logical foundations for declarative temporal logic programming languages. The key element in the deduction systems for temporal logic is to deal with eventualities and hidden invariants that may prevent the fulfillment of eventualities. Different ways of addressing this issue can be found in the works on deduction systems for temporal logic. Traditional tableau systems for temporal logic generate an auxiliary graph in a first pass.Then, in a second pass, unsatisfiable nodes are pruned. In particular, the second pass must check whether the eventualities are fulfilled. The one-pass tableau calculus introduced by S. Schwendimann requires an additional handling of information in order to detect cyclic branches that contain unfulfilled eventualities. Regarding traditional sequent calculi for temporal logic, the issue of eventualities and hidden invariants is tackled by making use of a kind of inference rules (mainly, invariant-based rules or infinitary rules) that complicates their automation. A remarkable consequence of using either a two-pass approach based on auxiliary graphs or aone-pass approach that requires an additional handling of information in the tableau framework, and either invariant-based rules or infinitary rules in the sequent framework, is that temporal logic fails to carry out the classical correspondence between tableaux and sequents. In this thesis, we first provide a one-pass tableau method TTM that instead of a graph obtains a cyclic tree to decide whether a set of PLTL-formulas is satisfiable. In TTM tableaux are classical-like. For unsatisfiable sets of formulas, TTM produces tableaux whose leaves contain a formula and its negation. In the case of satisfiable sets of formulas, TTM builds tableaux where each fully expanded open branch characterizes a collection of models for the set of formulas in the root. The tableau method TTM is complete and yields a decision procedure for PLTL. This tableau method is directly associated to a one-sided sequent calculus called TTC. Since TTM is free from all the structural rules that hinder the mechanization of deduction, e.g. weakening and contraction, then the resulting sequent calculus TTC is also free from this kind of structural rules. In particular, TTC is free of any kind of cut, including invariant-based cut. From the deduction system TTC, we obtain a two-sided sequent calculus GTC that preserves all these good freeness properties and is finitary, sound and complete for PLTL. Therefore, we show that the classical correspondence between tableaux and sequent calculi can be extended to temporal logic. The most fruitful approach in the literature on resolution methods for temporal logic, which was started with the seminal paper of M. Fisher, deals with PLTL and requires to generate invariants for performing resolution on eventualities. In this thesis, we present a new approach to resolution for PLTL. The main novelty of our approach is that we do not generate invariants for performing resolution on eventualities. Our method is based on the dual methods of tableaux and sequents for PLTL mentioned above. Our resolution method involves translation into a clausal normal form that is a direct extension of classical CNF. We first show that any PLTL-formula can be transformed into this clausal normal form. Then, we present our temporal resolution method, called TRS-resolution, that extends classical propositional resolution. Finally, we prove that TRS-resolution is sound and complete. In fact, it finishes for any input formula deciding its satisfiability, hence it gives rise to a new decision procedure for PLTL. In the field of temporal logic programming, the declarative proposals that provide a completeness result do not allow eventualities, whereas the proposals that follow the imperative future approach either restrict the use of eventualities or deal with them by calculating an upper bound based on the small model property for PLTL. In the latter, when the length of a derivation reaches the upper bound, the derivation is given up and backtracking is used to try another possible derivation. In this thesis we present a declarative propositional temporal logic programming language, called TeDiLog, that is a combination of the temporal and disjunctive paradigms in Logic Programming. We establish the logical foundations of our proposal by formally defining operational and logical semantics for TeDiLog and by proving their equivalence. Since TeDiLog is, syntactically, a sublanguage of PLTL, the logical semantics of TeDiLog is supported by PLTL logical consequence. The operational semantics of TeDiLog is based on TRS-resolution. TeDiLog allows both eventualities and always-formulas to occur in clause heads and also in clause bodies. To the best of our knowledge, TeDiLog is the first declarative temporal logic programming language that achieves this high degree of expressiveness. Since the tableau method presented in this thesis is able to detect that the fulfillment of an eventuality is prevented by a hidden invariant without checking for it by means of an extra process, since our finitary sequent calculi do not include invariant-based rules and since our resolution method dispenses with invariant generation, we say that our deduction methods are invariant-free.

From transistor to trapped-ion computers for quantum chemistry

Over the last few decades, quantum chemistry has progressed through the development of computational methods based on modern digital computers. However, these methods can hardly fulfill the exponentially-growing resource requirements when applied to large quantum systems. As pointed out by Feynman, this restriction is intrinsic to all computational models based on classical physics. Recently, the rapid advancement of trapped-ion technologies has opened new possibilities for quantum control and quantum simulations. Here, we present an efficient toolkit that exploits both the internal and motional degrees of freedom of trapped ions for solving problems in quantum chemistry, including molecular electronic structure, molecular dynamics, and vibronic coupling. We focus on applications that go beyond the capacity of classical computers, but may be realizable on state-of-the-art trapped-ion systems. These results allow us to envision a new paradigm of quantum chemistry that shifts from the current transistor to a near-future trapped-ion-based technology.

MPI parallel programming of mixed integer optimization problems using CPLEX with COIN-OR

The aim of this technical report is to present some detailed explanations in order to help to understand and use the Message Passing Interface (MPI) parallel programming for solving several mixed integer optimization problems. We have developed a C++ experimental code that uses the IBM ILOG CPLEX optimizer within the COmputational INfrastructure for Operations Research (COIN-OR) and MPI parallel computing for solving the optimization models under UNIX-like systems. The computational experience illustrates how can we solve 44 optimization problems which are asymmetric with respect to the number of integer and continuous variables and the number of constraints. We also report a comparative with the speedup and efficiency of several strategies implemented for some available number of threads.

First-principles study of the electronic and magnetic properties of defective carbon nanostructures

149 p.: graf.

Media translation and lesser-used languages: implications of subtitles for Irish language broadcastind

Eguíluz, Federico; Merino, Raquel; Olsen, Vickie; Pajares, Eterio; Santamaría, José Miguel (eds.)

First-principles study of the electronic structure and dynamical electronic excitations of strong spin-orbit metal Pb: bulk, surface and nanosized films

En la presente tesis se ha realizado el estudio de primeros principios (esto es, sinhacer uso de parámetros ajustables) de la estructura electrónica y la dinámica deexcitaciones electrónicas en plomo, tanto en volumen como en superficie y en formade películas de espesor nanométrico. Al presentar el plomo un número atómico alto(82), deben tenerse en cuenta los efectos relativistas. Con este fin, el doctorando haimplementado el acoplo espín-órbita en los códigos computacionales que hanrepresentado la principal herramienta de trabajo.En volumen, se han encontrado fuertes efectos relativistas asi como de lalocalización de los electrones, tanto en la respuesta dieléctrica (excitacioneselectrónicas colectivas) como en el tiempo de vida de electrones excitados. Lacomparación de nuestros resultados con medidas experimentales ha ayudado aprofundizar en dichos efectos.En el estudio de las películas a escala nanométrica se han hallado fuertes efectoscuánticos debido al confinamiento de los estados electrónicos. Dichos efectos semanifiestan tanto en el estado fundamental (en acuerdo con estudiosexperimentales), como en la respuesta dieléctrica a través de la aparición y dinámicade plasmones de diversas características. Los efectos relativistas, a pesar de no serimportantes en la estructura electrónica de las películas, son los responsables de ladesaparación del plasmón de baja energía en nuestros resultados.

Electronic spectroscopy of propofol, propofol homomers ad their hydratated clusters

538 p.

Processing Facilitation Strategies in OV and VO Languages: A Corpus Study

The present corpus study aimed to examine whether Basque (OV) resorts more often than Spanish (VO) to certain grammatical operations, in order to minimi ze the number of arguments to be processed before the verb. Ueno & Polinsky (2009) argue that VO/OV languages use certain grammatical resources with different frequencies in order to facilitate real-time processing. They observe that both OV and VO languages in their sample (Japanese, Turkish and Spanish) have a similar frequency of use of subject pro-drop; however, they find that OV languages (Japanese, Turkish) use more intransitive sentences than VO languages (English, Spanish), and conclude this is an OV-specific strategy to facilitate processing. We conducted a comparative corpus study of Spanish (VO) and Basque (OV). Results show (a) that the fre- quency of use of subject pro-drop is higher in Basque than in Spanish; and (b) Basque does not use more intransitive sentences than Spanish; both languages have a similar frequency of intransitive sentences. Based on these findings, we conclude that the frequency of use of grammatical resources to facilitate the processing does not depend on a single typological trait (VO/OV) but it is modulated by the concurrence of other grammatical feature.

Creating a German–Basque Electronic Dictionary for German Learners

Revista OJS

THE AINU LANGUAGES: TRADITIONAL RECONSTRUCTION, EURASIAN AREAL LINGUISTICS, AND DIACHRONIC (HOLISTIC) TYPOLOGY

El objetivo principal de esta tesis doctoral es, en primer lugar, ofrecer una reconstrucción alternativa del protoainu para, en segundo lugar, aplicar conceptos de tipología diacrónicaholística con el fin de discernir algún patrón evolutivo que ayude a responder a la pregunta:¿por qué la lengua ainu es como es en su contexto geolingüístico (lengua AOV con prefijos),cuando en la región euroasiática lo normal es encontrar el perfil 'lengua AOV con sufijos'? En suma, se trata de explorar las posibilidades que ofrece la tipología diacrónica holística,combinada con métodos más tradicionales, en la investigación de las etapas prehistóricas delenguas aisladas, es decir, sin parientes conocidos, como el ainu, el vasco, el zuñi o elburushaski. Este trabajo se divide en tres grandes bloques con un total de ocho capítulos, unapéndice con las nuevas reconstrucciones protoainúes y la bibliografía.El primer bloque se abre con el capítulo 1, donde se hace una breve presentación delas lenguas ainus y su filología. El capítulo 2 está dedicado a la reconstrucción de la fonologíaprotoainu. La reconstrucción pionera pertenece a A. Vovin (1992), que de hecho sirve comobase sobre la que ampliar, corregir o modificar nuevos elementos. En el capítulo 3 se describela morfología histórica de las lenguas ainus. En el capítulo 4 se investiga esta opción dentrode un marco más amplio que tiene como objetivo analizar los patrones elementales deformación de palabras. El capítulo 5, con el que se inicia el segundo bloque, da cabida a lapresentación de una hipótesis tipológica diacrónica, a cargo de P. Donegan y D. Stampe, conla que especialistas en lenguas munda y mon-khmer han sido capaces de alcanzar unreconstrucción del protoaustroasiático según la cual el tipo aglutinante de las lenguas mundasería secundario, frente al original monosilábico de las lenguas mon-khmer. En el capítulo 6se retoma la perspectiva tradicional de la lingüística geográfica, pero no se olvidan algunas delas consideraciones tipológicas apuntadas en el capítulo anterior (el hecho de que la hipótesisde Donegan y Stampe no funcione con el ainu no significa que la tipología diacrónica nopueda ser todavía de utilidad). En el capítulo 7 se presentan algunas incongruencias queresultan tras combinar las supuestas evidencias arqueológicas con el escenario lingüísticodescrito en capítulos anteriores. Las conclusiones generales se presentan en el capítulo 8. Elapéndice es una tabla comparativa con las dos reconstrucciones disponibles a fecha de hoypara la lengua protoainu, es decir, las propuestas por A. Vovin en su estudio seminal de 1992y en el capítulo 3 de la presente tesis. Dicha tabla incluye 686 reconstrucciones (puedehacerse una sencilla referencia cruzada con Vovin, puesto que ambas están ordenadasalfabéticamente).

Optimisation of the first principle code Octopus for massive parallel architectures: application to light harvesting complexes

150 p.

Proficiency, Attitude and Conventions in Minority Languages

In this paper we study a simple mathematical model of a bilingual community in which all agents are f luent in the majority language but only a fraction of the population has some degree of pro ficiency in the minority language. We investigate how different distributions of pro ficiency, combined with the speaker´attitudes towards or against the minority language, may infl uence its use in pair conversations.

Efficient electronic implementations of adaptive systems for ambient intelligence environments

183 p.

Electronic properties of graphene grain boundaries

Grain boundaries and defect lines in graphene are intensively studied for their novel electronic and magnetic properties. However, there is not a complete comprehension of the appearance of localized states along these defects. Graphene grain boundaries are herein seen as the outcome of matching two semi-infinite graphene sheets with different edges. We classify the energy spectra of grain boundaries into three different types, directly related to the combination of the four basic classes of spectra of graphene edges. From the specific geometry of the grains, we are able to obtain the band structure and the number of localized states close to the Fermi energy. This provides a new understanding of states localized at grain boundaries, showing that they are derived from the edge states of graphene. Such knowledge is crucial for the ultimate tailoring of electronic and optoelectronic applications.

Defect and structural imperfection effects on the electronic properties of BiTeI surfaces

The surface electronic structure of the narrow-gap seminconductor BiTeI exhibits a large Rashba-splitting which strongly depends on the surface termination. Here we report on a detailed investigation of the surface morphology and electronic properties of cleaved BiTeI single crystals by scanning tunneling microscopy, photoelectron spectroscopy (ARPES, XPS), electron diffraction (SPA-LEED) and density functional theory calculations. Our measurements confirm a previously reported coexistence of Te- and I-terminated surface areas