Combining statistical and semantic approaches to the translation of ontologies and taxonomies

Ontologies and taxonomies are widely used to organize concepts providing the basis for activities such as indexing, and as background knowledge for NLP tasks. As such, translation of these resources would prove useful to adapt these systems to new languages. However, we show that the nature of these resources is significantly different from the "free-text" paradigm used to train most statistical machine translation systems. In particular, we see significant differences in the linguistic nature of these resources and such resources have rich additional semantics. We demonstrate that as a result of these linguistic differences, standard SMT methods, in particular evaluation metrics, can produce poor performance. We then look to the task of leveraging these semantics for translation, which we approach in three ways: by adapting the translation system to the domain of the resource; by examining if semantics can help to predict the syntactic structure used in translation; and by evaluating if we can use existing translated taxonomies to disambiguate translations. We present some early results from these experiments, which shed light on the degree of success we may have with each approach

Using Cross-Lingual Explicit Semantic Analysis for Improving Ontology Translation

Semantic Web aims to allow machines to make inferences using the explicit conceptualisations contained in ontologies. By pointing to ontologies, Semantic Web-based applications are able to inter-operate and share common information easily. Nevertheless, multilingual semantic applications are still rare, owing to the fact that most online ontologies are monolingual in English. In order to solve this issue, techniques for ontology localisation and translation are needed. However, traditional machine translation is difficult to apply to ontologies, owing to the fact that ontology labels tend to be quite short in length and linguistically different from the free text paradigm. In this paper, we propose an approach to enhance machine translation of ontologies based on exploiting the well-structured concept descriptions contained in the ontology. In particular, our approach leverages the semantics contained in the ontology by using Cross Lingual Explicit Semantic Analysis (CLESA) for context-based disambiguation in phrase-based Statistical Machine Translation (SMT). The presented work is novel in the sense that application of CLESA in SMT has not been performed earlier to the best of our knowledge.

Residuos orgánicos como fuentes de fósforo

En este trabajo, se han llevado a cabo distintos experimentos en laboratorio, con el objetivo de estudiar el efecto de la aplicación de residuos orgánicos como fuentes de P en las pérdidas de este elemento, que se producen en suelo, tanto por escorrentía superficial como por lixiviación. El interés por evaluar las pérdidas de P se debe a la necesidad de conocer mejor los factores que influyen en los procesos de pérdidas de este elemento y así, poder reducir los problemas de eutrofización de aguas, tanto superficiales como subterráneas, provocadas por un exceso de este nutriente, junto con otros como el nitrógeno. Los trabajos experimentales que se han llevado a cabo se detallan a continuación: Se ha realizado el estudio de las formas de P contenidas en una serie de 14 residuos orgánicos, de distinto origen y tratamiento (compost, lodos, purines y digestato), comparando la información aportada por tres protocolos de fraccionamientos de P diferentes, seleccionados entre los principales métodos utilizados: protocolo de fraccionamiento de Ruttemberg (1992), protocolo de Normas, medidas y ensayos (Ruban et al., 2001a) y protocolo de Huang et al. (2008). Todos los métodos de fraccionamiento empleados aportaron información útil para conocer las formas de P de los residuos, a pesar de que alguno de ellos fue descrito para sedimentos o suelos. Sin embargo, resulta difícil comparar los resultados entre unos y otros, ya que cada uno emplea extractantes y tiempos de ensayos diferentes. Las cantidades de P total determinadas por cada método mantienen una relación lineal, aunque el método SMT, por ser más directo, obtiene las cantidades más elevadas para todos los residuos. Los métodos secuenciales (métodos de Huang y Ruttemberg), a pesar de ser más largos y tediosos, aportan información más detallada de la disponibilidad de las formas de P, y con ello, permiten obtener una mejor estimación de las pérdidas potenciales de este elemento tras su aplicación en suelo. Se han encontrado relaciones positivas entre las fracciones determinadas por estos dos métodos. Así mismo, se encuentra una correlación entre las formas solubles de P y la concentración de los iones [Ca + Fe + Al] de los residuos, útiles como indicadores de la disponibilidad de este elemento. Sin embargo, el protocolo SMT, no obtiene información de la solubilidad o disponibilidad de las formas de P contenidas, ni las formas determinadas mantienen relaciones directas con las de los otros métodos, con excepción del P total. Para el estudio del comportamiento de los residuos aplicados en suelos, se pusieron a punto sistemas de lluvia simulada, con el objetivo de caracterizar las pérdidas de P en la escorrentía superficial generada. Por otra parte, se emplearon columnas de suelos enmendados con residuos orgánicos, para el estudio de las pérdidas de P por lixiviación. Los ensayos de simulación de lluvia se llevaron a cabo de acuerdo al “National Phosphorus Research proyect“ (2001), que consigue simular eventos sucesivos de lluvia en unas condiciones semejantes a la realidad, empleando cajas llenas de suelo del horizonte superficial, con residuos aplicados tanto superficialmente como mediante mezcla con el propio suelo. Los ensayos se realizaron con seis residuos de diferente naturaleza y sometidos a distintos tratamientos. Se encontraron diferencias significativas en las pérdidas de las formas de P analizadas, tanto disueltas como particuladas, en las aguas de escorrentía generadas. En general, las pérdidas en el primer evento de lluvia tras la aplicación de los residuos fueron mayores a las generadas en el segundo evento, predominando las formas de P particuladas respecto a las disueltas en ambos. Se encontró una relación positiva entre las pérdidas de P en las aguas de escorrentía generadas en cada ensayo, con los contenidos de P soluble en agua y fácilmente disponible de los residuos empleados, determinados por los protocolos de fraccionamientos secuenciales. Además, se emplearon los modelos matemáticos desarrollados por Vadas et al. (2005, 2007), de evaluación de las pérdidas de P por escorrentía para fertilizantes y estiércoles. La predicción de estos modelos no se cumple en el caso de todos los residuos. Las distintas propiedades físicas de los residuos pueden afectar a las diferencias entre las pérdidas experimentales y las esperadas. Los ensayos de simulación del proceso de lixiviación se llevaron a cabo en columnas de percolación, con suelos enmendados con residuos orgánicos, de acuerdo a la norma “CEN/TS 14405–2004: Caracterización de los residuos – Test de comportamiento de lixiviación – Test de flujo ascendente”. Las pérdidas de P por procesos de lixiviación de agua, han sido despreciadas durante mucho tiempo respecto a las pérdidas por escorrentía. Sin embargo, se ha demostrado que deben tenerse en consideración, principalmente en algunos tipos de suelos o zonas cercanas a acuíferos. Se utilizaron tres suelos de distinta procedencia para los ensayos, de manera que se pudo estudiar la influencia del tipo de suelo en las pérdidas de P para cada tipo de residuo (purín, compost, digestato y lodo de EDAR). Los índices de adsorción de P determinados para cada suelo permiten evaluar aquellos que presentarán más riesgo de producir pérdidas de este elemento al aplicarse fuentes externas de P, encontrando una relación positiva entre ambos. Las pérdidas de P en los lixiviados varían en función tanto del residuo como del suelo empleado. Para el compost, el purín y el lodo, se encontró una relación entre las pérdidas generadas en el agua lixiviada de las columnas y las formas de P soluble contenidas en los residuos. Sin embargo, en el caso del digestato, no existía esta correlación. Las pérdidas para este residuo fueron en todos los casos menores a las estimadas, considerando las formas de P contenido. El estudio de la mojabilidad, propiedad física del residuo que evalúa la capacidad de interacción residuo-agua, permitió explicar el comportamiento anómalo de este residuo, con una mayor resistencia a que el agua entrara en su estructura y por tanto, una mayor dificultad de solubilizar el P contenido en el propio residuo, que en el caso de otros residuos. En general, podemos considerar que el estudio de las formas de P más disponibles o solubles en agua, aporta información útil de las pérdidas potenciales de P. Sin embargo, es necesario estudiar las propiedades físicas de los residuos orgánicos aplicados y la capacidad de adsorción de P de los suelos, para estimar las pérdidas de P y con ello, colaborar a controlar los procesos de eutrofización en aguas. ABSTRACT This dissertation explores the effect of organic wastes application as sources of P in losses of this element that occur by both surface runoff and leaching in soil. To do so, diverse laboratory experiments are conducted and presented here. Evaluating P losses is necessary to better understand the factors that influence the processes behind the loss of this element. Reducing P losses reduces eutrophication problems of both surface water and groundwater caused by an excess of this nutrient, along with other as nitrogen. Details of the experiments are presented below: The first experiment studies the forms of P contained in a series of 14 organic wastes of different origin and treatment (compost, sludge, slurry and digestate), comparing the information provided by three methods of P fractionation. The methods selected were: Ruttemberg protocol (1992); Standards, Measurements and Testing protocol (Ruban et al., 2001a); and Huang protocol (Huang et al., 2008). All fractionation methods employed successfully contribute to our knowledge of P forms in wastes, even though one of them was originally described for sediments or soils information. However, it is difficult to compare results among each other, as each protocol employs different extractants and time in the trials. Total amounts of P obtained by each method show a linear relationship, although the SMT method, which is more direct, obtains the highest amounts for all residues. Sequential methods (Huang and Ruttemberg’s protocols), despite being longer and more tedious, provide more detailed information on the availability of the forms of P. Therefore, allow the estimation of the potential losses of P after application in soil. Furthermore, positive relationships have been found among fractions obtained by these methods. Positive relationship has been found also among soluble forms of P and the concentration of ions Fe + Ca + Al, which is useful as an indicator of the availability of this element. However, the SMT protocol does not collect information about solubility or availability of forms of P contained; neither do certain forms maintain direct relations with the forms from other methods, with the exception of total P methods. To study the behavior of wastes applied to soils two experiments were conducted. Simulated rain systems were prepared to characterize P losses in the surface runoff generated. In addition, columns of soils amended with organic waste were developed for the study of P leaching losses. Simulated rain systems were carried out according to the ’National Phosphorus Research Project’ (2001), which manages to simulate successive rainfall events in conditions resembling reality. The experiment uses boxes filled with soil from the surface horizon amended with residues, both superficially and by mixing with the soil. Tests were conducted with six residues of different type and subjected to diverse treatments. Findings show significant differences in losses of the P forms analyzed in the generated runoff water, in both solution and particulate forms. In general, losses in the first rainfall event after application of waste were higher than the losses generated in the second event, predominating particulate forms of P over dissolved forms in both events. In all trials, a positive relationship was found between various P forms determined by sequential fractionation protocols (water soluble P and readily available P forms) and P losses in runoff. Furthermore, results from Vadas´s mathematical models (Vadas et al., 2005; 2007) to assess P losses by runoff fertilizers and manures indicate that the prediction of this model is not fulfilled in the case of all residues. The diverse physical properties of wastes may affect the differences between experimental and expected losses. Finally, leaching simulation processes were carried out in percolation columns, filled with soils amended with organic wastes, following the ‘CEN/TS 14405-2004 standard: Characterization of waste - Leaching behavior test - Test Flow ascending ’. P losses by leaching have been neglected for a long time with respect to runoff losses. However, findings corroborate previous studies showing that these P losses have to be taken into account, especially in certain types of soils and in zones near aquifers. To study the influence of soil type on P losses, experiments were carried out with three different soils and for each type of waste (manure, compost, digestate and sludge WWTP). Each soil’s P adsorption rates allow assessing which soils imply a higher risk of P losses when external sources of P are applied. P losses in leachate vary according to the type of soil employed and according to the specific residue. In the case of compost, manure and sludge, there is a relationship between leaching losses and residues’ soluble forms of P. The exception being the digestate, where there was no such correlation. Digestate P losses by leaching were lower than expected in all cases considering the forms of P contained. Moreover, examining digestate wettability -- that is, the physical property of the residue that assesses the capacity of waste-water interaction -- allowed explaining the anomalous behavior of this residue. Digestate has a high resistance to water entering its structure and thus higher difficulty to solubilize the P contained. Overall, studying the more available or soluble P forms provides useful information about the potential loss of P. However, this dissertation shows that it is necessary to examine the physical properties of organic residues applied as well as the P adsorption capacity of soils to estimate P losses, and thus to control eutrophication in water.

Formal Verification of Temporal Properties for Parametrized Concurrent Programs and Concurrent Data Structures

Los tipos de datos concurrentes son implementaciones concurrentes de las abstracciones de datos clásicas, con la diferencia de que han sido específicamente diseñados para aprovechar el gran paralelismo disponible en las modernas arquitecturas multiprocesador y multinúcleo. La correcta manipulación de los tipos de datos concurrentes resulta esencial para demostrar la completa corrección de los sistemas de software que los utilizan. Una de las mayores dificultades a la hora de diseñar y verificar tipos de datos concurrentes surge de la necesidad de tener que razonar acerca de un número arbitrario de procesos que invocan estos tipos de datos de manera concurrente. Esto requiere considerar sistemas parametrizados. En este trabajo estudiamos la verificación formal de propiedades temporales de sistemas concurrentes parametrizados, poniendo especial énfasis en programas que manipulan estructuras de datos concurrentes. La principal dificultad a la hora de razonar acerca de sistemas concurrentes parametrizados proviene de la interacción entre el gran nivel de concurrencia que éstos poseen y la necesidad de razonar al mismo tiempo acerca de la memoria dinámica. La verificación de sistemas parametrizados resulta en sí un problema desafiante debido a que requiere razonar acerca de estructuras de datos complejas que son accedidas y modificadas por un numero ilimitado de procesos que manipulan de manera simultánea el contenido de la memoria dinámica empleando métodos de sincronización poco estructurados. En este trabajo, presentamos un marco formal basado en métodos deductivos capaz de ocuparse de la verificación de propiedades de safety y liveness de sistemas concurrentes parametrizados que manejan estructuras de datos complejas. Nuestro marco formal incluye reglas de prueba y técnicas especialmente adaptadas para sistemas parametrizados, las cuales trabajan en colaboración con procedimientos de decisión especialmente diseñados para analizar complejas estructuras de datos concurrentes. Un aspecto novedoso de nuestro marco formal es que efectúa una clara diferenciación entre el análisis del flujo de control del programa y el análisis de los datos que se manejan. El flujo de control del programa se analiza utilizando reglas de prueba y técnicas de verificación deductivas especialmente diseñadas para lidiar con sistemas parametrizados. Comenzando a partir de un programa concurrente y la especificación de una propiedad temporal, nuestras técnicas deductivas son capaces de generar un conjunto finito de condiciones de verificación cuya validez implican la satisfacción de dicha especificación temporal por parte de cualquier sistema, sin importar el número de procesos que formen parte del sistema. Las condiciones de verificación generadas se corresponden con los datos manipulados. Estudiamos el diseño de procedimientos de decisión especializados capaces de lidiar con estas condiciones de verificación de manera completamente automática. Investigamos teorías decidibles capaces de describir propiedades de tipos de datos complejos que manipulan punteros, tales como implementaciones imperativas de pilas, colas, listas y skiplists. Para cada una de estas teorías presentamos un procedimiento de decisión y una implementación práctica construida sobre SMT solvers. Estos procedimientos de decisión son finalmente utilizados para verificar de manera automática las condiciones de verificación generadas por nuestras técnicas de verificación parametrizada. Para concluir, demostramos como utilizando nuestro marco formal es posible probar no solo propiedades de safety sino además de liveness en algunas versiones de protocolos de exclusión mutua y programas que manipulan estructuras de datos concurrentes. El enfoque que presentamos en este trabajo resulta ser muy general y puede ser aplicado para verificar un amplio rango de tipos de datos concurrentes similares. Abstract Concurrent data types are concurrent implementations of classical data abstractions, specifically designed to exploit the great deal of parallelism available in modern multiprocessor and multi-core architectures. The correct manipulation of concurrent data types is essential for the overall correctness of the software system built using them. A major difficulty in designing and verifying concurrent data types arises by the need to reason about any number of threads invoking the data type simultaneously, which requires considering parametrized systems. In this work we study the formal verification of temporal properties of parametrized concurrent systems, with a special focus on programs that manipulate concurrent data structures. The main difficulty to reason about concurrent parametrized systems comes from the combination of their inherently high concurrency and the manipulation of dynamic memory. This parametrized verification problem is very challenging, because it requires to reason about complex concurrent data structures being accessed and modified by threads which simultaneously manipulate the heap using unstructured synchronization methods. In this work, we present a formal framework based on deductive methods which is capable of dealing with the verification of safety and liveness properties of concurrent parametrized systems that manipulate complex data structures. Our framework includes special proof rules and techniques adapted for parametrized systems which work in collaboration with specialized decision procedures for complex data structures. A novel aspect of our framework is that it cleanly differentiates the analysis of the program control flow from the analysis of the data being manipulated. The program control flow is analyzed using deductive proof rules and verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, our techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. The verification conditions correspond to the data manipulation. We study the design of specialized decision procedures to deal with these verification conditions fully automatically. We investigate decidable theories capable of describing rich properties of complex pointer based data types such as stacks, queues, lists and skiplists. For each of these theories we present a decision procedure, and its practical implementation on top of existing SMT solvers. These decision procedures are ultimately used for automatically verifying the verification conditions generated by our specialized parametrized verification techniques. Finally, we show how using our framework it is possible to prove not only safety but also liveness properties of concurrent versions of some mutual exclusion protocols and programs that manipulate concurrent data structures. The approach we present in this work is very general, and can be applied to verify a wide range of similar concurrent data types.