Aquesta Tesi que pretén proporcionar un conjunt de tècniques per enfrontar-se al problema que suposa la variació del color en les imatges preses des d'una plataforma mòbil per causa del canvi en les condicions d'il·luminació entre diverses vistes d'una certa escena preses en diferents instants i posicions. També tracta el problema de la segmentació de imatges de color per a poder-les utilitzar en tasques associades a les capacitats d'un robot mòbil, com ara la identificació d'objectes o la recuperació d'imatges d'una gran base de dades.Per dur a terme aquests objectius, primerament s'estableix matemàticament la transformació entre colors degut a variacions d'il·luminació. Així es proposa un model continu per la generació del senyal de color com a generalització natural d'altres propostes anteriors. D'aquesta manera es pot estudiar matemàticament i amb generalitat les condicions per l'existència, unicitat i bon comportament de les solucions, i expressar qualsevol tipus d'aplicació entre colors, independentment del tipus de discretització. Així, queda palès la relació íntima entre el problema de la invariància de color i el de la recuperació espectral, que també es planteja a la pràctica. El model desenvolupat es contrasta numèricament amb els de regressió lineal, en termes d'errors de predicció.Un cop establert el model general, s'opta per un model lineal simplificat a l'hora de realitzar els càlculs pràctics i permet alleugerir el nombre dels mateixos. En particular, el mètode proposat es basa en trobar la transformació més probable entre dues imatges a partir del càlcul d'un conjunt de transformacions possibles i de l'estimació de la freqüència i grau d'efectivitat de cadascuna d'elles. Posteriorment, es selecciona el millor candidat d'acord amb la seva versemblança. L'aplicació resultant serveix per transformar els colors de la imatge tal i com es veuria sota les condicions d'il·luminació canòniques.Una vegada el color de les imatges d'una mateixa escena es manté constant, cal procedir a la seva segmentació per extreure'n la informació corresponent a les regions amb color homogeni. En aquesta Tesi es suggereix un algorisme basat en la partició de l'arbre d'expansió mínima d'una imatge mitjançant una mesura local de la probabilitat de les unions entre components. La idea és arribar a una segmentació coherent amb les regions reals, compromís entre particions amb moltes components (sobresegmentades) i amb molt poques (subsegmentades). Un altre objectiu és que l'algorisme sigui prou ràpid com per ser útil en aplicacions de robòtica mòbil. Aquesta característica s'assoleix amb un plantejament local del creixement de regions, tot i que el resultat presenti caràcters globals (color). La possible sobresegmentació es suavitza gràcies al factor probabilístic introduït.L'algorisme de segmentació també hauria de generar segmentacions estables en el temps. Així, l'algorisme referit s'ha ampliat incloent-hi un pas intermedi entre segmentacions que permet de relacionar regions semblants en imatges diferents i propagar cap endavant els reagrupaments de regions fets en anteriors imatges, així si en una imatge unes regions s'agrupen formant-ne una de sola, les regions corresponents en la imatge següent també s'han d'agrupar juntes. D'aquesta manera, dues segmentacions correlatives s'assemblen i es pot mantenir estable la segmentació d'una seqüència.Finalment, es planteja el problema de comparar imatges a partir del seu contingut. Aquesta Tesi es concentra només en la informació de color i, a més de investigar la millor distància entre segmentacions, es busca també mostrar com la invariància de color afecta les segmentacions.Els resultats obtinguts per cada objectiu proposat en aquesta Tesi avalen els punts de vista defensats, i mostren la utilitat dels algorismes, així com el model de color tant per la recuperació espectral com pel càlcul explícit de les transformacions entre colors. / This Thesis endeavors providing a set of techniques for facing the problem of color variation in images taken from a mobile platform and caused by the change in the conditions of lighting among several views of a certain scene taken at different instants and positions. It also treats the problem of segmenting color images in order to use them in tasks associated with the capacities of a mobile robot, such as object identification or image retrieval from a large database.In order to carry out these goals, first transformation among colors due to light variations is mathematically established. Thus, a continuous model for the generation of color is proposed as a natural generalization of other former models. In this way, conditions for the existence, uniqueness, and good behavior of the solutions can be mathematically studied with a great generality, and any type of applications among colors can be expressed independently of the discretization scheme applied. Thus, the intimate relation among the problem of color invariance and that of spectral recovery is made evident and studied in practice too. The developed model is numerically contrasted with those of a least squares linear regression in terms of prediction errors.Once the general model is established, a simplified linear version is chosen instead for carrying out the practical calculations while lightening the number of them. In particular, the proposed method is based on finding the likeliest transformation between two images from the calculation of a set of feasible transformations and the estimation of the frequency and the effectiveness degree of each of them. Later, the best candidate is selected in accordance with its likelihood. The resulting application is then able to transform the image colors as they would be seen under the canonical light.After keeping the image colors from a scene constant, it is necessary to proceed to their segmentation to extract information corresponding to regions with homogeneous colors. In this Thesis, an algorithm based on the partition of the minimum spanning tree of an image through a local measure of the likelihood of the unions among components is suggested. The idea is to arrive at a segmentation coherent with the real regions, a trade-off between partitions with many component (oversegmented) and those with fewer components (subsegmented).Another goal is that of obtaining an algorithm fast enough to be useful in applications of mobile robotics. This characteristic is attained by a local approach to region growing, even though the result still shows global feature (color). The possible oversegmentation is softened thanks to a probabilistic factor.The segmentation algorithm should also generate stable segmentations through time. Thus, the aforementioned algorithm has been widened by including an intermediate step that allows to relate similar regions in different images and to propagate forwards the regrouping of regions made in previous images. This way, if in some image some regions are grouped forming only one bigger region, the corresponding regions in the following image will also be grouped together. In this way, two correlatives segmentations resemble each other, keeping the whole segmented sequence stabler.Finally, the problem of comparing images via their content is also studied in this Thesis, focusing on the color information and, besides investigating which is for our aims the best distance between segmentation, also showing how color constancy affects segmentations. The results obtained in each of the goals proposed in this Thesis guarantee the exposed points of view, and show the utility of the algorithms suggested, as well as the color model for the spectral recovery and the explicit calculation of the transformations among colors.

Últimamente se ha incrementado considerablemente la utilización de la inteligencia artificial en los campos de la electrónica de potencia y de los sistemas de control de la velocidad y del posicionamiento. Estos métodos, basados en sistemas expertos, la lógica difusa y las redes neuronales artificiales, necesitan una gran base de datos o conocimientos que describan el funcionamiento del sistema junto a un análisis lógico, en lugar del análisis matemático, para controlar el sistema y facilitar la toma de decisiones. Uno de estos métodos corresponde a las redes neuronales artificiales.En esta tesis doctoral se presenta la aplicación de redes neuronales artificiales en los sistemas de control vectorial y control directo del par para una máquina de inducción. Esta tecnología, relativamente nueva, sirve para poder reemplazar eficientemente algunos equipos analógicos ya existentes. Los datos necesarios para entrenar las redes neuronales artificiales se obtienen, en primer lugar, de los resultados de las simulaciones del sistema formado por el motor y su control, y en segundo lugar, a partir de los resultados experimentales. A tal fin se implementa un modelo del motor de inducción que se prueba con motores de diferentes valores nominales y se controla con diferentes sistema de control: control vectorial por el método indirecto con y sin realimentación de velocidad, control vectorial por el método directo con realimentación de velocidad y control directo del par. Para el caso de los sistemas del control vectorial por el método indirecto, con y sin realimentación de velocidad se han utilizado redes neuronales artificiales de respuesta a impulso finito (FIRANN) para emular algunos bloques de los sistemas del control vectorial tales como la estimación de referencia de corriente estator. Cada red neuronal artificial se ha diseñado, entrenado y probado como una parte del conjunto del sistema de control. Con respecto al control vectorial por el método directo y con realimentación de velocidad, se estima la referencia de la corriente del estator y también se realiza la mayor parte del control vectorial con redes neuronales artificiales FIRANN. Cada red neuronal artificial se ha diseñado, entrenado y probado como una parte del conjunto del sistema de control.Para el sistema de control directo del par se han utilizado redes neuronales artificiales de propagación hacia adelante (MFANN) que emulan la tabla de conmutación del ondulador, la transformación de las tensiones en el sistema de referencia "abc" al sistema de referencia fijado al estator "dq", la transformación de las corrientes de estator en el sistema de referencia "abc" al sistema de referencia fijado al estator "dq" y por último, un estimador de par. Estas cuatro redes neuronales se probaron en línea tanto de forma independiente como conjuntamente. Su comportamiento ha sido bueno en comparación con el sistema sin redes neuronales. Además, se realizó la implementación física del equipo para el control en tiempo real de un motor de inducción por el método directo clásico, y usando redes neuronales mediante una tarjeta dSPACE "DS1103". Este montaje ha permitido hacer las medidas necesarias para poder comparar el comportamiento del sistema bajo las alternativas propuestas. / Recently, the use of artificial intelligence has been increased in the fields of power electronics, and position and speed control systems. These methods, based on expert systems, fuzzy logic and artificial neural networks, require a large data base or knowledge to describe the operation of the system, besides to the logic analysis instead of the mathematical analysis in order to control the system and facilitate the decision tasks. One of these methods are the artificial neural networks.This doctoral thesis shows the aplication of artificial neural networks to the vector control systems and direct torque control of induction machines. This technology is useful to replace some existing analogical equipment in an efficient way. The data needed to train the artificial neural networks is obtained in the first place from the simulation results of the system, and in the second place from the experimental results. For that purpose, it was implemented an induction motor model which is tested with different machine characteristics, and it is controlled with different control systems: indirect method vector control with and without speed feedback, direct method vector control with speed feedback and direct torque control.For indirect method vector control with and without speed feedback, it has been used finite impulse response artificial neural networks (FIRANN) to emulate some blocks of the vector control systems such as the estimation of the stator current. Each artificial neural network has been designed, trained and tested as a part of the control system set.For the case of direct method vector control with speed feedback, the stator current reference and the majority of the vector control is realized also with artificial neural networks FIRANN. Each artificial neural network has been designed, trained and tested as a part of the control system set.In the direct torque control, it has been used feed-forward artificial neural networks (MFANN) to emulate the commutation table of the inverter, to develop the transformation of the voltages from the "abc" reference frame to the "dq" reference frame, and the transformation of the stator currents from the "abc" reference frame to the "dq" reference frame, and finally, to estimate the torque. These four neural networks have been tested online in an independent way and also as a whole. Its performance has been good in comparison with the system without neural networks.Finally, it was realized a physical implementation of the equipment for real time control of an induction motor by the classical method and by artificial neural networks using a dSPACE "DS1103" card. This implementation has allowed realize the measurements to be able to compare the performance of the system under the different proposed alternatives.

Las actitudes, el conocimiento y las acciones generalmente se basan en muestras. Algunos basan sus conclusiones en muestras pequeñas y pocas veces toman en cuenta la magnitud de lo que se desconoce. Generalmente se carece de recursos para estudiar más de una parte del problema de interés que pudiera aumentar nuestro conocimiento. Algunas razones para el uso de las técnicas de muestreo son: costo reducido, mayor velocidad, mayor enfoque o perspectiva y mayor exactitud.La fusión de datos surge como una alternativa a la fuente única de datos frente a la necesidad de conseguir el máximo de información posible al menor costo. Tiene como objetivo combinar datos de diferentes fuentes para poder disponer de toda la información en un solo archivo, aunque artificial, con todas las variables de interés. Utiliza lo mejor de la información existente en un archivo para reconstruir la información ausente en otro archivo. Es una estimación estadística de los datos faltantes. Es un medio de limitar la recolección de datos, reconstruyendo la información faltante. No es un problema de análisis estadístico con datos faltantes en el cual se consideran los mecanismos que conducen a la ausencia de datos. En el caso de la fusión de datos, se presentan bloques completos de datos ausentes, en general, muestras independientes.La revisión bibliográfica ha permitido analizar el problema del análisis de datos faltantes como una aproximación al tema de la fusión de datos, considerando que la fusión de datos es un caso particular. En este caso, se está hablando de bloques de datos faltantes y en muchas ocasiones, datos faltantes por diseño.El objetivo de la fusión de datos es por lo tanto, el obtener un solo archivo que pueda ser analizado posteriormente con herramientas de minería de datos. La idea es estimar los valores de las variables no informadas (valores faltantes) a partir de un bloque de variables informadas correlacionadas con el bloque de variables a reconstituir (variables comunes). Es importante hacer notar que no se esta generando nueva información.Parte de este trabajo se dedica a la definición y aproximación del concepto fusión de datos. Se presentan algunos enfoques para el tratamiento de los datos ausentes. Se han revisado, de manera no exhaustiva, algunas técnicas relacionadas con el tema y se muestran aplicaciones de la fusión de datos relacionadas con otras herramientas.Son muchas las técnicas que existen para tratar la reconstrucción de los datos faltantes. En este trabajo, el enfoque se ha hecho sobre la técnica de imputación Hot deck. Con esta técnica se sustituyen valores individuales extraídos de unidades observadas similares. Se basa en el reemplazo de la información faltante en el conjunto de individuos no informados (con datos faltantes) que se llaman receptores, utilizando la información de los individuos informados más parecidos, llamados donantes. Es una práctica común que involucra esquemas elaborados para la selección de las unidades similares para la imputación. Se estudian algunos procedimientos no paramétricos de discriminación para efectuar la búsqueda de los individuos más cercanos (parecidos). Existen distintos algoritmos diseñados para esto. Se ha hecho una revisión de algunos de estos métodos de búsqueda. Este trabajo se basa en el algoritmo de Fukunaga/Narendra. Se muestran los componentes del sistema. Se presentan los fundamentos y las bases que se han seguido para el desarrollo y la implantación del mismo. Se han establecido algunas propuestas no paramétricas para la medición de la calidad de la fusión.La experimentación y prueba de las distintas propuesta se ha hecho dividida en dos partes. En una se ha hecho una selección aleatoria de los individuos para formar un conjunto de donantes y un conjunto de receptores. En la segunda parte, la selección se ha hecho a partir de una característica específica en una variable. Para esto se emplea un archivo sintético creado a partir de un conjunto de datos privados de financiación para el otorgamiento de créditos al consumo. Este archivo general consta de 6692 individuos. El aspecto práctico de este trabajo, ha sido el desarrollo de un sistema de fusión de datos.Aunque mucho está escrito sobre la imputación Hot deck, siempre habrá espacio para proponer nuevos métodos. Evaluar la calidad de la fusión seguirá siendo tema de interés. Queda claro que la fusión de datos satisface la necesidad de muchos de proporcionar una sola fuente de datos completa a los usuarios finales. Sin embargo, se debe tener cuidado al hacer uso de esta información (son estimaciones, no valores reales observados). / Very often, attitudes, knowledge and actions, are base on samples. Some base their conclusions on small samples and are less likely to be aware of the extent of what is unknown. There is frequently a lack of resources to study more than a part of the problem of interest which could increase our knowledge of it. Some reasons for the use of sample techniques are: reduced cost, greater speed, greater scope o perspective and greater accuracy. Data fusion emerges as an alternative to single source data, faced to the need of acquiring the more information as possible at the lower cost. Its objective is to combine data from different sources in order to have the whole information on a single file, though artificial, but with all the variables of interest. It makes use of the best of the current information contained on one file to rebuild the missing information on another file. It's a statistical estimation of the missing data. It is a mean to restrict the gathering of data, rebuilding the missing information. It is not a problem of statistical analysis with missing data, on which, the process that leads to the absence of data are considered. In the case of data fusion, complete blocks of missing data appear, generally, independent samples.The bibliography has allowed analyzing the subject of missing data as an approach to the subject of data fusion, considering that data fusion is a particular case of it. In this case, missing data and sometimes missing by design is what it is all about.Therefore, the objective of data fusion is to get a single file which can be analyzed further with data mining tools. The idea is to estimate the values of the variables with missing data upon a block of variables with the whole information correlated with the variables to be rebuilt. It is important to mention that new information is not being generated. A part of this work is dedicated to the definition and rapprochement to the concept of data fusion. Some ways of treating the problem of missing data are presented. Some techniques related to the subject have been reviewed in a non exhaustive way and some data fusion applications related with other tools is shown.There are many techniques for treating the rebuilding of missing data. This work is focused on the hot deck technique.With this technique, individual units, took from similar observed units are replaced. It is based on the replacement of the missing information in the set of units with missing information called receivers, using the information of units more likely to them called donors. It is a common practice that involves complex outlines for the selection of the similar unit to be used for the imputation.Some non parametric discrimination procedures have been studied to perform the search of the nearest units (the most resembling). There are different algorithms for this purpose. A review of some of these search methods has been made. This work is based on the Fukunaga/Narendra algorithm. The components of the system are shown as well as the foundations and bases followed for the development and implementation. Some non parametric proposals have been made for measuring the quality of the fusion.The experimentation and tests of the system has been made in two parts. In one part, a random selection of the units that makes the set of donors and the set of receivers has been made. In the second part, the selection has been made upon a specific characteristic on a variable. For this purpose, a synthetic file created upon a set of private financing data for the grant of consumer goods credits is used. This general file contains 6692 units.The practical aspect of this work has been the development of a data fusion system. Although many have been written about hot deck imputation, there is always room for new proposals. Evaluating the quality of the fusion is still a subject of interest. It is clear that data fusion fulfill the need of many to provide the final user with a complete single source of data. However, care must be taken with the use of this information (they are estimations, not actual observed values).

DE TESIS DOCTORALA partir de la aplicación de la metodología ergonómica, este estudio se dedicó a investigar propuestas para mejorar la accesibilidad y legibilidad de la información académica para los estudiantes universitarios con discapacidad, que solicitaron ayuda al Plan de Apoyo al Estudiante con Discapacidad de la UPC, - proyecto experimental que objetiva aminorar problemática de dicho alumnado en el proceso de aprendizaje / enseñanza.El grupo estudiado fue compuesto por 14 alumnos discapacitados físicos y/o sensoriales matriculados en las escuelas y centros adscritos de la Universitat Politècnica de Catalunya, entre los 22 atendidos por el Plan de Apoyo al Estudiante con Discapacidad de la UPC, que desearon participar y colaborar con esta investigación llevada a cabo entre los cursos académicos de 1999/2000 y 2001/2002.La originalidad del trabajo científico consiste en que la metodología ergonómica no ha sido aplicada anteriormente para la adaptación del puesto de estudio del estudiante universitario con necesidades educativas especiales por motivo de discapacidad, física y/o sensorial.Como objetivos generales y específicos, esta investigación se propuso a recompilar y analizar las dificultades del alumnado descrito como sujetos, en relación con el acceso y legibilidad de la información académica, y proponer un diseño ergonómico de la información que permita al grupo estudiado aminorar sus dificultades de participación en el proceso aprendizaje/enseñanza.Para ello, fue utilizado el "método etnográfico" aplicado en la metodología de la ciencia de la Ergonomía Cognitiva. En la composición de la investigación, se utilizaron las técnicas de investigación "observación", "aplicación de entrevistas" y "análisis de tarea", para estudiar casos presentados por alumnos disminuidos física, cognitiva y sensorialmente, matriculados en la Universitat Politècnica de Catalunya, UPC, durante los cursos académicos de 2000/2001 y 2001/2002. Las conclusiones muestran la idoneidad del método ergonómico para la descripción de las necesidades del alumnado delimitado. 100% de los sujetos estudiados describen una percepción de mejora en la accesibilidad y legibilidad de la información académica, a partir de las actuaciones ergonómicas propuestas y utilizadas, derivadas de las investigaciones realizadas. Se prevé que se produzca un éxito similar en la adaptación del puesto de estudio de los alumnos con las características mencionadas, con la aplicación del método desarrollado.El trabajo se concluye con la proposición de sugerencias en los métodos, técnicas y equipos utilizados en el proceso de enseñanza / aprendizaje que, incorporadas al sistema de educación universitario ordinario, podrían facilitar el acceso y la legibilidad de la información académica para dicho alumnado.En consecuencia de los resultados significativos encontrados, esta investigación se derivó en la publicación de tres artículos científicos publicados en Barcelona, por ocasión de los siguientes eventos:CAES¨99 - Congreso Internacional de Ergonomía,Les Tecnologies de la Informació i les Comunicacions en l´Educació - Jornades de Treball1º Congreso Internacional de Docencia Universitaria.

A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKS En el desarrollo formal de software, la especificación formal se utiliza con fines de verificación y validación. Se han definido diferentes tipos de especificaciones formales. En esta tesis nos centraremos en especificaciones algebraicas. Este tipo de especificaciones formales son especificaciones axiomáticas, que suelen definirse en un lenguaje de especificación que incluye diferentes operadores de estructuración. La semántica de estos operadores se define de una forma que sea lo más independiente posible de la lógica de especificación o institución. Otra etapa fundamental en métodos formales es el diseño de software. Las tareas básicas que suelen realizarse durante esta etapa son la deducción de propiedades a partir de una especificación, el refinamiento de especificaciones o verificar que un programa satisface una especificación. Entendemos por entorno de diseño algebraico a un formalismo que incluye la definición de un lenguaje de especificación algebraica con semántica formal y la definición implícita o explícita de, al menos, las dos primeras de las tres tareas de diseño mencionadas anteriormente. Es importante que la definición de los entornos de diseño algebraico sea tambien lo más independiente posible de la lógica del lenguaje de especificación y, si es el caso, que la definición sea para una clase arbitraria de lenguajes de programación. El entorno de diseño algebraico con el que trabajaremos en esta tesis está basado en un lenguaje de especificación muy sencillo que ha sido utilizado para dar semántica a otros lenguajes de especificación de más alto nivel. El principal objetivo de esta tesis es definir un marco formal que permite reusar demostradores de teoremas para teorías de tipos con tipos dependientes e inductivos para el desarrollo de demostradores de teoremas para entornos de diseño algebraico. El problema puede considerarse interesante por varios motivos. Primero, esperamos que el desarrollo de este tipo de herramientas incrementará el uso de este tipo de métodos formales. Segundo, la investigación a realizar es completamente diferente a los trabajos realizados anteriormente y por último, el trabajo requiere un conocimiento extenso de una familia de formalismos no standard que forman las diferentes teorías de tipos con tipos dependientes que se han definido. En esta tesis, primero presentamos de forma general, las características basicas y las aplicaciones de las diferentes teorías de tipos con tipos dependientes. Estudiamos con más detalle la teoría de tipos que vamos a utilizar en el resto de la tesis, y a continuación presentamos un nuevo principio de codificación de sistemas de demostración finitos para la teoría de tipos escogida que mejora algunas de las limitaciones de otros principios de codificación existentes.Con el fin de comparar de forma abstracta las diferentes semánticas dadas a ciertos operadores de comportamiento del lenguaje de especificación escogido, definimos una institución a la que denominamos institución algebraica de comportamiento. Esta institución es también útil para definir las formas normales de las especificaciones que son necesarias para definir cierta clase de sistemas de demostración. A continuación, presentamos diferentes sistemas de demostración para la deducción de propiedades a partir de especificaciones y para el refinamiento de especificaciones. La principal aportación en esta parteconsiste en rediseñar los sistemas de demostración que no es posible dar representaciones adecuadas en la teoría de tipos escogida por ser sistemas de demostración infinitarios.Finalmente, damos una representación en la teoría de tipos de los sistemas de demostración más significativos de nuestro entorno de diseño algebraico usando el nuevo principio de codificación presentado en la tesis. Esto nos permite reutilizar los demostradores de teoremas de la teoría de tipos escogida para el desarrollo de demostradores de teoremas del entorno de diseño algebraico escogido. A TYPE -THEORETIC APPROACH TO PROOF SUPPORT FOR ALGEBRAIC DESIGN FRAMEWORKSIn software engineering, a formal specification of what a system has to do plays a crucial role in the software development process. Formality is required for verification and validation purposes. Different forms of formal specifications have been developed. This thesis concentrates on the algeraic approach to system specification. In essence, this approach can be characterized by:· Axiomatic specifications which consist of a signature together with a set of axioms in a specification logic which any implementation of the system with that specification has to satisfy.· Operations to combine and modify specifications from subspecifications with an algebraic semantics.· An abstract presentation of the semantics as independent as possible of the specification logic or institution.Another crucial step in the software development process is software design. Some of the usual tasks which are performed during software design are the following: deduction of properties from specifications, refinement of specifications and verification of a program with respect to a specification. We understand by an algebraic design framework a formalism which includes a formal definition of an algebraic specification language including a model-theoretic semantics and the implicit or explicit formal definition of at least the two first software design tasks. The definition of algebraic design frameworks should be for several specification logics or even better for an arbitrary but fixed institution, and if it is the case for an arbitrary class of programming languages. In the literature, there exists a large amount of algebraic specification languages and algebraic design frameworks. The algebraic design framework which we will work in this thesis will be based on a kernel and simple algebraic specification language. The main objective of this thesis is to give an approach to reuse theorem provers for type theories with dependent and inductive types for the development of theorem provers for algebraic design frameworks. The problem can be considered interesting for several reasons. First, we believe that the development of tools in type-theoretic theorem provers will help to spread the use of algebraic techniques. Note that these kind of theorem provers have been widely used and applied. Second, the work to be done is completely different to the work done before and finally this work requires a thorough understanding of a non-standard family of formalisms which are type theories. In this thesis, first we give an overall view of type theories together with their apllications and then we present a new principle of encoding in an expressive type theory which solves some of the limitations of previous principle of encodings. In order to give a generic presentation of the framework of ASL for different specification logics, we give an abstract semantic framework in which the semantics of the the behavioural operators of ASL can be uniformly instantiated in first-order and higher-order logic. We also redesign the different proof systems for deduction and refinement when it is not possible to give adequate encodings in the type theory because they are infinatary proof systems. In some cases, different solutions are given for first and higher-order logics. Finally, the main proof systems of the algebraic design framework for ASL have been encoded in UTT using the new principle of encoding presented in the thesis. This allows us to take advantage of the current implementation of theorem provers for UTT to implement proof checkers for the proof systems of our chosen algebraic design framework.

Monoterpene secoiridoid biosynthesis contributes the terpene component of terpenoid indole alkaloids produced in the medicinal plant Catharanthus roseus. The thesis focuses on the development of fundamental knowledge and methodology to reconstruct the monoterpene secoiridoid pathway in tobacco plants using metabolic engineering. The thrust of the thesis concentrated on remaining challenges to engineer complex secondary metabolic pathways in plants. We focused on the early part of the pathway and we recovered a population of transgenic tobacco plants expressing different combinations of transgenes. Analysis at metabolomic and transcriptomic levels provided novel insights into remaining bottlenecks for the effective engineering of secondary metabolic pathways in plants. The experimental part of the thesis is complemented by the development of a systematic patent search to create an IP database with all relevant patents related with the engineering of terpenoid indole alkaloid pathway in plants. / La biosíntesi dels monoterpens secoiridoïdes aporta el compost terpè dels terpens índole alcaloides produïts per la planta medicinal Catharanthus roseus. La tesi es centra en el desenvolupament dels coneixements fonamentals i la metodologia per reconstruir la ruta metabòlica dels monoterpens secoiridoïdes en plantes de tabac mitjançant enginyeria metabòlica. La idea central de la tesi enfoca els reptes pendents de l'enginyeria de rutes metabòliques complexes en plantes. Centrant-nos en la primera part de la ruta, es va regenerar una població de plantes de tabac transgèniques expressant diferents combinacions de transgens. L'anàlisi a nivell metabolòmic i transcriptòmic ens proporciona nous coneixements per resoldre les dificultats que encara hi ha en l’enginyeria efectiva de les rutes metabòliques secundàries a les plantes. La part experimental de la tesi es complementa amb el desenvolupament d'una recerca sistemàtica de patents, per crear una base de dades de IP, amb totes les patents pertinents relacionades amb l'enginyeria de la ruta metabòlica dels terpens índole alcaloides en plantes. / La biosíntesis de monoterpenos secoiridoides aporta el compuesto terpeno de los terpenos índole alcaloides producidos por la planta medicinal Catharanthus roseus. La tesis se centra en el desarrollo de los conocimientos fundamentales i la metodología para reconstruir la ruta metabólica de los monoterpenos secoiridoides en plantas de tabaco mediante ingeniería metabólica. La idea central de la tesis enfoca en los retos pendientes de la ingeniería de rutas metabólicas complejas en plantas. Centrándonos en la primera parte de la ruta, regeneramos una población de plantas de tabaco transgénicas expresando diferentes combinaciones de transgenes. El análisis a nivel metabolómico y transcriptómico nos proporciona nuevos conocimientos para resolver las dificultades que todavía encuentra la ingeniería efectiva de las rutas metabólicas secundarias en las plantas. La parte experimental de la tesis se complementa con el desarrollo de una búsqueda sistemática de patentes, para crear una base de datos de IP, con todas las patentes pertinentes relacionadas con la ingeniería de la ruta metabólica de los terpenos índole alcaloides en plantas.

Aquest treball investiga si els traductors professionals de papiament de Curaçao actuen com a agents de transferència lèxica i també si ho fan d'una manera servil. La recerca adopta un enfocament de mètodes mixts que es triangulen. L'aspecte quantitatiu de la mateixa es desenvolupa en base la resposta del qüestionari d'una mostra de 205 traductors i no traductors. L'aspecte qualitatiu es basa en una pregunta oberta en el qüestionari, una mostra de tres entrevistes planificadors lingüístics governamentals i en una selecció de textos en apapiamento (no)traduïts. Els resultats mostren que els traductors fan més transferències lèxiques que els no traductors, i que el prestigi del llenguatge, la sensibilitat amb el text, l'estabilitat laboral, l'experiència professional i la formació formal juguen un paper important en això. A més, en última instància, són els planificadors lingüístics els que accepten o rebutgen per consens l'admissió formal de tots els elements lèxics al papiament. Però en general, la transferència lèxica d’anglès a papiament implica una participació activa i agència del traductor que es passa per alt i que no reflecteix una actitud servil. / Este trabajo investiga si los traductores profesionales de papiamento de Curazao actúan como agentes de transferencia léxica y también si lo hacen de una manera servil. La investigación adopta un enfoque de métodos mixtos que se triangulan. El aspecto cuantitativo de la misma se desarrolla en base la respuesta del cuestionario de una muestra de 205 traductores y no traductores. El aspecto cualitativo se basa en una pregunta abierta en el cuestionario, una muestra de tres entrevistas planificadores lingüísticos gubernamentales y en una selección de textos en papiamento (no)traducidos. Los resultados muestran que los traductores hacen más transferencias léxicas que los no traductores, y que el prestigio del lenguaje, la sensibilidad con el texto, la estabilidad laboral, la experiencia profesional y la formación formal juegan un papel importante en ello. Además, en última instancia, son los planificadores lingüísticos los que aceptan o rechazan por consenso la admisión formal de todos los elementos léxicos en el papiamento. Pero en general, la transferencia léxica Inglés-a-papiamento implica una participación activa y agencia del traductor que se pasa por alto y que no refleja una actitud servil. / This research investigates whether professional Curaçaoan Papiamentu translators act as agents of lexical transfer in Papiamentu and also whether they do so in a subservient manner. The research adopts a mixed-methods approach and is triangulated. The quantitative aspect of it develops on a questionnaire sample of 205 translators and non-translators. The qualitative aspect builds on an open-ended question on the questionnaire, an interview sample of three official language planners and on selected Papiamentu (non)translated texts. The results show that the translators make more lexical transfers than do the non-translators, and that language prestige, text sensitivity, employment stability, professional experience and formal training play important roles in this. Further, it is ultimately the language planners who carry out by consensus the formal admission of all lexical items into Papiamentu. But generally what English-to-Papiamentu lexical transfer implies is an overlooked agentive involvement of the translators rather than translator subservience in this process.

El método de descomposición de dominios (DD) que se propone en esta tesis pretende resolver flujos incompresibles alrededor de objetos en movimiento relativo. El algoritmo de DD está basado en un acoplamiento del tipo Dirichlet/Neumann(Robin) aplicado a subdominios con solapamiento, y es, por tanto, una extensión del método Dirichlet/Neumann(Robin) clásico con subdominios disjuntos. En realidad, el campo de aplicación de este estudio es mucho más amplio puesto que en el se propone un posible marco teórico para abordar la extensión a subdominios solapados de los métodos mixtos clásicos: métodos Dirichlet/Robin, Dirichlet/Neumann, Robin/Neumann y Robin/Robin. Se observa que los métodos mixtos propuestos heredan propiedades del método de Schwarz y al mismo tiempo conservan el comportamiento de sus equivalentes sin solapamiento cuando este tiende a cero. Se muestra como resultado principal que el solapamiento hace estos métodos más robustos que los métodos sin solapamiento. El método de DD que se estudia es geométrico y algorítmico. Es geométrico en el sentido de que la partición del dominio computacional se lleva a cabo antes del proceso de mallado y de acuerdo con el acoplamiento de DD que se prevé usar. Es también algorítmico porque la solución en cada subdominio se obtiene en procesos diferentes y el intercambio de información entre subdominios se realiza mediante un código maestro. Tal estrategia es muy flexible puesto que requiere muy pocas modificaciones del código numérico original. Por consiguiente, sólo el código maestro necesita ser adaptado a los códigos y estrategias numéricos utilizados en cada subdominio. Se presenta una descripción detallada de la implementación del método de DD propuesto en el contexto numérico de los elementos finitos. Presentamos técnicas de interpolación para los datos de tipo Dirichlet y Neumann y desarrollamos algoritmos de conservación. Una vez el acoplamiento de DD y las interpolaciones definidos, presentamos un método del tipo Chimera para la resolución de flujos alrededor de objetos en movimiento. En particular, definimos transformaciones tensoriales para transformar variables de un subdominio a otro. Finalmente, el algoritmo de DD se aplica a un código implícito para la resolución de las ecuaciones de Navier-Stokes incompresibles y también a las ecuaciones de Navier-Stokes promediadas con un modelo de turbulencia de una ecuación. / The domain decomposition (DD) method we present in this work aims at solving incompressible flows around objects in relative motion. The DD algorithm is based on a Dirichlet/Neumann(Robin) coupling applied to overlapping subdomains. Hence, it is an extension of the classical Dirichlet/Neumann(Robin) method which uses disjoint subdomains. Actually, the field of application of this work is wider as it proposes to set up a possible theoretical framework for studying the overlapping extensions of classical mixed methods: the Dirichlet/Robin, Dirichlet/Neumann, Robin/Neumann and Robin/Robin DD methods. We observe that mixed DD methods inherit some properties of the Schwarz method while they keep the behavior of the classical mixed DD methods when the overlap tends to zero. As a main result, we show that the overlap makes the proposed methods more robust than disjoint mixed DD methods. The DD method we propose is geometric and algorithmic. It is geometric because the partition of the computational domain is performed before the meshing, and in accordance to the DD coupling. It is also algorithmic because the solution on each subdomain is obtained on separate processes and the exchange of information between the subdomains is carried out by a Master code. This strategy is very flexible as it requires almost no modification to the original numerical code. Therefore, only the Master code has to be adapted to the numerical codes and strategies used on each subdomain. We present a detailed description of the implementation of the DD methods in the numerical framework of finite elements. We present interpolation techniques for Dirichlet and Neumann data as well as conservation algorithms. Once the domain decomposition coupling and interpolation techniques are defined, we set up a Chimera method for the solution of the flow over objets in relative movements. Tensorial transformations are introduced to be able to express variables measures in one subdomain. Finally, the DD algorithm is applied to an implicit finite element code for the solution of the Navier-Stokes equations and also of the Reynolds Averaged Navier-Stokes equations together with a one-equation turbulence model.

This Ph.D. thesis mainly deals with temporal and deductive databases areas and the aim is to obtain a method for integrity constraint checking in bitemporal deductive databases, analyzing the temporal integrity constraint behavior. The existence of a transaction time dimension is especially useful to reduce the number of transition rules. In the valid time dimension, the temporal dependence of database predicate terms has been explored. Moreover, this Ph.D. thesis provides some research advances bringing together the areas of temporal databases and data warehouses. Chapter 1 is an introduction to the problem and the related work of this Ph.D. thesis main area. Chapter 2 presents temporal databases, and chapter 3 deductive databases. Chapter 4 introduces the study of temporal deductive database transaction behavior, explaining the concept of coherent transaction. This concept is used to reject transactions without more information requirements. Chapter 5 defines a new taxonomy of temporal integrity constraints to achieve a better understanding of why constraints are required and a best way to define them using first-order logic. In order to meet these goals, we have studied temporal integrity constraint taxonomies existing on the temporal database area and other deeply related areas such as multiversion databases. These works have been adapted and further developed to cover the scope of bitemporal deductive databases. Chapter 6 proposes an integrity constraint checking method for bitemporal deductive databases that derives a set of transition rules for each temporal integrity constraint. Then, Standard Linear Deduction with Negation as Failure Resolution is used to verify that a transaction does not violate any constraint before the transaction is allowed to commit. The set of transition rules obtained is very large; therefore, a carefully analysis of the integrity constraints using the taxonomy introduced above drastically reduces the number of rules. This chapter includes some examples of this new reduced set of transition rules and application examples of our integrity constraint checking method in bitemporal deductive databases. In chapters 7 and 8, we present our current and further work. In chapter 7, we identify a new type of predicate term dependent of time. This new type of term, named temporally dependent term, is formally defined and deeply studied in order to find its properties and its applicability to queries and integrity constraints. In chapter 8, we explain how to combine temporal database and data warehouse areas. Finally, chapter 9 provides conclusions and further work.

L'obesitat representa un greu problema de salut. Una de les seves comorbiditats més importants és la malaltia no alcohòlica del fetge gras que s'associa amb una alta morbiditat i mortalitat. Un mètode no invasiu per al diagnòstic d'aquesta malaltia milloraria l'atenció clínica i la metabolòmica ha sorgit com una poderosa eina per a la cerca de nous biomarcadors. En aquesta línia, mitjançant un estudi metabolòmic proposem al a-cetoglutarat com un nou biomarcador; la quantificació d'aquest biomarcador pot potenciar la recerca de nous enfocaments terapèutics, disminuir la necessitat d'una biòpsia de fetge i els seus inconvenients i pot ser útil en l'avaluació de la progressió d'aquesta malaltia hepàtica. La ingesta d'energia excessiva molt comú en el nostre dia a dia, altera l'homeòstasi metabòlica i condueix a un estat inflamatori crònic, que té un paper important en el desenvolupament de malalties com l'obesitat i la malaltia no alcohòlica del fetge gras. Per aquesta raó, l'avaluació del paper de la inflamació crònica en models animals alimentats amb una dieta rica en greix podria suggerir noves estratègies terapèutiques. En aquest sentit, hem desenvolupat un ratolí transgènic que sobreexpressa CCL2 en tots els teixits. Aquest estudi va contribuir al coneixement sobre la relació entre la inflamació i el metabolisme i va suggerir una sèrie de preguntes per a futurs estudis. Finalment i per tal de determinar si els efectes nocius causats per una sobreexpressió de CCL2 combinada amb un excés d'energia es poden contrarestar per l'absència de CCR2, vam generar un altre model animal que sobreexpressa CCL2 però que a la vegada és deficient per CCR2. Els resultats van demostrar que els trastorns metabòlics observats en el model transgènic eren revertits per la inhibició de la funció biològica de l'eix CCL2/CCR2. D’aquesta manera els moduladors de CCR2 podrien convertir-se en nous agents terapèutics. / La obesidad es un grave problema de salud. Una de sus comorbididades más importantes es la enfermedad hepática no alcohólica (EHNA) y se asocia con una alta morbilidad y mortalidad. Por ello, un método no invasivo para el diagnóstico de esta enfermedad mejoraría la atención clínica y la metabolómica ha surgido como una poderosa herramienta para la búsqueda de biomarcadores. Mediante un estudio metabólomico proponemos al a-cetoglutarato como un nuevo biomarcador, la quantificación de este biomarcador puede potenciar la búsqueda de nuevos enfoques terapéuticos, disminuir la necesidad de una biopsia de hígado y puede ser útil en la evaluación de la progresión de esta enfermedad. La ingesta de energía excesiva muy común en nuestro día a día, altera la homeostasis metabólica y conduce a un estado inflamatorio crónico, que tiene un papel importante en el desarrollo de enfermedades como la obesidad y la EHNA. Por esta razón, la evaluación del papel de la inflamación crónica en modelos animales alimentados con una dieta rica en grasa podría sugerir nuevas estrategias terapéuticas. Por ello, hemos desarrollado un ratón transgénico que sobreexpresa CCL2 en todos los tejidos. Éste estudio contribuyó al conocimiento sobre la relación entre la inflamación y el metabolismo y sugirió una serie de preguntas para futuros estudios. Por último y con el fin de determinar si los efectos nocivos causados por una sobreexpresión de CCL2 combinada con un exceso de energía se pueden contrarrestar por la ausencia de CCR2, creamos otro modelo animal que sobreexpresa CCL2 pero que a la vez deficiente para CCR2. Los resultados demostraron que los trastornos metabólicos observados en los ratones transgénicos eran contrarestados por la inhibición de la función biológica del eje CCL2/CCR2. De este modo los moduladores CCR2 podrían convertirse en nuevos agentes terapéuticos. / Obesity severely affects human health, and the accompanying non-alcoholic liver disease (NAFLD) is associated with high morbidity and mortality. For this reason, a non-invasive method to detect this liver impairment may substantially improve clinical care and metabolomics has emerged as a powerful tool for discovering novel biomarkers. Accordingly, using metabolomics approaches, we propose plasma a-ketoglutarate as a novel biomarker for the detection of NAFLD. The measurement of this biomarker may potentiate the search for novel therapeutic approaches, may decrease the need for liver biopsy overcoming its drawbacks and may be useful in the assessment of disease progression. Furthermore, the excessive energy intake, that nowadays is a part of current human lifestyle, alters metabolic homeostasis and leads to a state of low-grade inflammations which has an important role in the development of diseases such as obesity and NAFLD. For this reason, the assessment of the role of chronic inflammation in animal models fed an energy surplus could suggest novel therapeutic strategies for the management. In this way, we generated a targeted CCL2 transgenic mouse which overexpresses CCL2 in all tissue which contributed to the knowledge about the relationship between inflammation and metabolism and suggested a number of mechanistic questions for future study. Finally, in order to determine if the deleterious metabolic effects caused by a continuous and ubiquitous expression of CCL2 combined with energy surplus can be counteract by the absence of CCR2, we created a CCL2 overexpressor but, at the same time, CCR2 knock-out mouse. Results of this study suggested that all metabolic disturbances observed in transgenic mice which overexpress CCL2 could be reverted by the inhibition of CCL2/CCR2 axis biologic function. All this information could be really important to establish CCR2 modulators as a new class of therapeutic agents to the management of metabolic disease.