Low-temperature experiments of sediment core GeoB6229-6 at the South American continental margin off the Rio de la Plata estuary

With various low-temperature experiments performed on magnetic mineral extracts of marine sedimentary deposits from the Argentine continental slope near the Rio de la Plata estuary, a so far unreported style of partial magnetic self-reversal has been detected. In these sediments the sulphate-methane transition (SMT) zone is situated at depths between 4 and 8 m, where reductive diagenesis severely alters the magnetic mineral assemblage. Throughout the sediment column magnetite and ilmenite are present together with titanomagnetite and titanohematite of varying compositions. In the SMT zone (titano-)magnetite only occurs as inclusions in a siliceous matrix and as intergrowths with lamellar ilmenite and titanium-rich titanohematite, originating from high temperature deuteric oxidation within the volcanic host rocks. These abundant structures were visualized by scanning electron microscopy and analysed by energy dispersive spectroscopy. Warming of field-cooled and zero-field-cooled low-temperature saturation remanence displays magnetic phase transitions of titanium-rich titanohematite below 50 K and the Verwey transition of magnetite. A prominent irreversible decline characterizes zero-field cooling of room temperature saturation remanence. It typically sets out at ~210 K and is most clearly developed in the lower part of the SMT zone, where low-temperature hysteresis measurements identified ~210 K as the blocking temperature range of a titanohematite phase with a Curie temperature of around 240 K. The mechanism responsible for the marked loss of remanence is, therefore, sought in partial magnetic self-reversal by magnetostatic interaction of (titano-)magnetite and titanohematite. When titanohematite becomes ferrimagnetic upon cooling, its spontaneous magnetic moments order antiparallel to the (titano-)magnetite remanence causing an drastic initial decrease of global magnetization. The loss of remanence during subsequent further cooling appears to result from two combined effects (1) magnetic interaction between the two phases by which the (titano-)magnetite domain structure is substantially modified and (2) low-temperature demagnetization of (titano-)magnetite due to decreasing magnetocrystalline anisotropy. The depletion of titanomagnetite and superior preservation of titanohematite is characteristic for strongly reducing sedimentary environments. Typical residuals of magnetic mineral assemblages derived from basaltic volcanics will be intergrowths of titanohematite lamellae with titanomagnetite relics. Low-temperature remanence cycling is, therefore, proposed as a diagnostic method to magnetically characterize such alteration (palaeo-)environments.

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.

An SmtB-like repressor from Synechocystis PCC 6803 regulates a zinc exporter

ORF slr0798, now designated ziaA, from Synechocystis PCC 6803 encodes a polypeptide with sequence features of heavy metal transporting P-type ATPases. Increased Zn2+ tolerance and reduced 65Zn accumulation was observed in Synechococcus PCC 7942, strain R2-PIM8(smt), containing ziaA and upstream regulatory sequences, compared with control cells. Conversely, reduced Zn2+ tolerance was observed following disruption of ziaA in Synechocystis PCC 6803, and ziaA-mediated restoration of Zn2+ tolerance has subsequently been used as a selectable marker for transformation. Nucleotide sequences upstream of ziaA, fused to a promoterless lacZ gene, conferred Zn2+-dependent β-galactosidase activity when introduced into R2-PIM8(smt). The product of ORF sll0792, designated ZiaR, is a Zn2+-responsive repressor of ziaA transcription. Reporter gene constructs lacking ziaR conferred elevated Zn2+-independent expression from the ziaA operator–promoter in R2-PIM8(smt). Gel retardation assays detected ZiaR-dependent complexes forming with the zia operator–promoter and ZiaR–DNA binding was enhanced by treatment with a metal-chelator in vitro. Two mutants of ZiaR (C71S/C73S and H116R) bound to, and repressed expression from, the ziaA operator–promoter but were unable to sense Zn2+. Metal coordination to His-imidazole and Cys-thiolate ligands at these residues of ZiaR is thus implicated in Zn2+-perception by Synechocystis PCC 6803.

Phrase-based statistical machine translation: explanation of its processes and statistical models and evaluation of the English to Spanish translations produced

Statistical machine translation (SMT) is an approach to Machine Translation (MT) that uses statistical models whose parameter estimation is based on the analysis of existing human translations (contained in bilingual corpora). From a translation student’s standpoint, this dissertation aims to explain how a phrase-based SMT system works, to determine the role of the statistical models it uses in the translation process and to assess the quality of the translations provided that system is trained with in-domain goodquality corpora. To that end, a phrase-based SMT system based on Moses has been trained and subsequently used for the English to Spanish translation of two texts related in topic to the training data. Finally, the quality of this output texts produced by the system has been assessed through a quantitative evaluation carried out with three different automatic evaluation measures and a qualitative evaluation based on the Multidimensional Quality Metrics (MQM).

Effets de la stimulation magnétique transcrânienne dans la maladie de Parkinson avec déficits cognitifs légers

Beaucoup de patients atteints de la maladie de Parkinson (MP) peuvent souffrir de troubles cognitifs dès les étapes initiales de la maladie et jusqu’à 80% d’entre eux vont développer une démence. Des altérations fonctionnelles au niveau du cortex préfrontal dorsolatéral (CPFDL), possiblement en relation avec le noyau caudé, seraient à l’origine de certains de ces déficits cognitifs. Des résultats antérieurs de notre groupe ont montré une augmentation de l’activité et de la connectivité dans la boucle cortico-striatale cognitive suite à la stimulation magnétique transcrânienne (SMT) utilisant des paramètres « theta burst » intermittent (iTBS) sur le CPFDL gauche. Pour cette étude, 24 patients atteints de la MP avec des troubles cognitifs ont été séparées en 2 groupes : le groupe iTBS active (N=15) et le groupe sham (stimulation simulée, N=9). Une batterie neuropsychologique détaillée évaluant cinq domaines cognitifs (attention, fonctions exécutives, langage, mémoire et habiletés visuo-spatiales) a été administrée lors des jours 1, 8, 17 et 37. Le protocole iTBS a été appliqué sur le CPFDL gauche durant les jours 2, 4 et 7. Les scores z ont été calculés pour chaque domaine cognitif et pour la cognition globale. Les résultats ont montré une augmentation significative de la cognition globale jusqu’à 10 jours suivant l’iTBS active, particulièrement au niveau de l’attention, des fonctions exécutives et des habiletés visuo-spatiales. Cet effet sur la cognition globale n’est pas répliqué dans le groupe sham. Ces résultats suggèrent donc que l’iTBS peut moduler la performance cognitive chez les patients atteints de MP avec des déficits cognitifs.

Depth profiles of dissolved sulfide and sulfate in the pore water of hydrocarbon seep sediments offshore Pakistan

The interaction between fluid seepage, bottom water redox, and chemosynthetic communities was studied at cold seeps across one of the world's largest oxygen minimum zones (OMZ) located at the Makran convergent continental margin. Push cores were obtained from seeps within and below the core-OMZ with a remotely operated vehicle. Extracted sediment pore water was analyzed for sulfide and sulfate concentrations. Depending on oxygen availability in the bottom water, seeps were either colonized by microbial mats or by mats and macrofauna. The latter, including ampharetid polychaetes and vesicomyid clams, occurred in distinct benthic habitats, which were arranged in a concentric fashion around gas orifices. At most sites colonized by microbial mats, hydrogen sulfide was exported into the bottom water. Where macrofauna was widely abundant, hydrogen sulfide was retained within the sediment. Numerical modeling of pore water profiles was performed in order to assess rates of fluid advection and bioirrigation. While the magnitude of upward fluid flow decreased from 11 cm yr**-1 to <1 cm yr**-1 and the sulfate/methane transition (SMT) deepened with increasing distance from the central gas orifice, the fluxes of sulfate into the SMT did not significantly differ (6.6-9.3 mol m**-2 yr**-1). Depth-integrated rates of bioirrigation increased from 120 cm yr**-1 in the central habitat, characterized by microbial mats and sparse macrofauna, to 297 cm yr**-1 in the habitat of large and few small vesicomyid clams. These results reveal that chemosynthetic macrofauna inhabiting the outer seep habitats below the core-OMZ efficiently bioirrigate and thus transport sulfate down into the upper 10 to 15 cm of the sediment. In this way the animals deal with the lower upward flux of methane in outer habitats by stimulating rates of anaerobic oxidation of methane (AOM) with sulfate high enough to provide hydrogen sulfide for chemosynthesis. Through bioirrigation, macrofauna engineer their geochemical environment and fuel upward sulfide flux via AOM. Furthermore, due to the introduction of oxygenated bottom water into the sediment via bioirrigation, the depth of the sulfide sink gradually deepens towards outer habitats. We therefore suggest that - in addition to the oxygen levels in the water column, which determine whether macrofaunal communities can develop or not - it is the depth of the SMT and thus of sulfide production that determines which chemosynthetic communities are able to exploit the sulfide at depth. We hypothesize that large vesicomyid clams, by efficiently expanding the sulfate zone down into the sediment, could cut off smaller or less mobile organisms, as e.g. small clams and sulfur bacteria, from the sulfide source.

Analogical Reasoning Techniques in Intelligent Counterterrorism Systems

The paper develops a set of ideas and techniques supporting analogical reasoning throughout the life-cycle of terrorist acts. Implementation of these ideas and techniques can enhance the intellectual level of computer-based systems for a wide range of personnel dealing with various aspects of the problem of terrorism and its effects. The method combines techniques of structure-sensitive distributed representations in the framework of Associative-Projective Neural Networks, and knowledge obtained through the progress in analogical reasoning, in particular the Structure Mapping Theory. The impact of these analogical reasoning tools on the efforts to minimize the effects of terrorist acts on civilian population is expected by facilitating knowledge acquisition and formation of terrorism-related knowledge bases, as well as supporting the processes of analysis, decision making, and reasoning with those knowledge bases for users at various levels of expertise before, during, and after terrorist acts.

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.

Sediment and pore water chemistry of cores 214 and 755 recovered during Meteor M72/1 and POSEIDON cruise POS317/2, northwestern Black Sea

High-resolution sedimentary records of major and minor elements (Al, Ba, Ca, Sr, Ti), total organic carbon (TOC), and profiles of pore water constituents (SO42-, CH4, Ca2+, Ba2+, Mg2+, alkalinity) were obtained for two gravity cores (core 755, 501 m water depth and core 214, 1686 m water depth) from the northwestern Black Sea. The records were examined in order to gain insight into the cycling of Ba in anoxic marine sediments characterized by a shallow sulfate-methane transition (SMT) as well as the applicability of barite as a primary productivity proxy in such a setting. The Ba records are strongly overprinted by diagenetic barite (BaSO4) precipitation and remobilization; authigenic Ba enrichments were found at both sites at and slightly above the current SMT. Transport reaction modeling was applied to simulate the migration of the SMT during the changing geochemical conditions after the Holocene seawater intrusion into the Black Sea. Based on this, sediment intervals affected by diagenetic Ba redistribution were identified. Results reveal that the intense overprint of Ba and Baxs (Ba excess above detrital average) strongly limits its correlation to primary productivity. These findings have implications for other modern and ancient anoxic basins, such as sections covering the Oceanic Anoxic Events for which Ba is frequently used as a primary productivity indicator. Our study also demonstrates the limitations concerning the use of Baxs as a tracer for downward migrations of the SMT: due to high sedimentation rates at the investigated sites, diagenetic barite fronts are buried below the SMT within a relatively short period. Thus, 'relict' barite fronts would only be preserved for a few thousands of years, if at all.

Physical oceanography, pore water chemistry and water column methane turover rates during POLARSTERN cruise ANT-XXIX/4

Recent studies have suggested that the marine contribution of methane from shallow regions and melting marine terminating glaciers may have been underestimated. Here we report on methane sources and potential sinks associated with methane seeps in Cumberland Bay, South Georgia's largest fjord system. The average organic carbon content in the upper 8 meters of the sediment is around 0.65 wt.%; this observation combined with Parasound data suggest that the methane gas accumulations probably originate from peat-bearing sediments currently located several tens of meters below the seafloor. Only one of our cores indicates upward advection; instead most of the methane is transported via diffusion. Sulfate and methane flux estimates indicate that a large fraction of methane is consumed by anaerobic oxidation of methane (AOM). Carbon cycling at the sulfate-methane transition (SMT) results in a marked fractionation of the d13C-CH4 from an estimated source value of -65 per mil to a value as low as -96 per mil just below the SMT. Methane concentrations in sediments are high, especially close to the seepage sites (~40 mM); however, concentrations in the water column are relatively low (max. 58 nM) and can be observed only close to the seafloor. Methane is trapped in the lowermost water mass, however, measured microbial oxidation rates reveal very low activity with an average turnover of 3.1 years. We therefore infer that methane must be transported out of the bay in the bottom water layer. A mean sea-air flux of only 0.005 nM/m²/s confirms that almost no methane reaches the atmosphere.

High-resolution pore-water and solid-phase analyses of sediment cores GeoB6520-3 (Hydrate Hole) and GeoB6521-2 (Worm Hole) of the northern Congo Fan

The geochemical cycling of barium was investigated in sediments of pockmarks of the northern Congo Fan, characterized by surface and subsurface gas hydrates, chemosynthetic fauna, and authigenic carbonates. Two gravity cores retrieved from the so-called Hydrate Hole and Worm Hole pockmarks were examined using high-resolution pore-water and solid-phase analyses. The results indicate that, although gas hydrates in the study area are stable with respect to pressure and temperature, they are and have been subject to dissolution due to methane-undersaturated pore waters. The process significantly driving dissolution is the anaerobic oxidation of methane (AOM) above the shallowest hydrate-bearing sediment layer. It is suggested that episodic seep events temporarily increase the upward flux of methane, and induce hydrate formation close to the sediment surface. AOM establishes at a sediment depth where the upward flux of methane from the uppermost hydrate layer counterbalances the downward flux of seawater sulfate. After seepage ceases, AOM continues to consume methane at the sulfate/methane transition (SMT) above the hydrates, thereby driving the progressive dissolution of the hydrates "from above". As a result the SMT migrates downward, leaving behind enrichments of authigenic barite and carbonates that typically precipitate at this biogeochemical reaction front. Calculation of the time needed to produce the observed solid-phase barium enrichments above the present-day depths of the SMT served to track the net downward migration of the SMT and to estimate the total time of hydrate dissolution in the recovered sediments. Methane fluxes were higher, and the SMT was located closer to the sediment surface in the past at both sites. Active seepage and hydrate formation are inferred to have occurred only a few thousands of years ago at the Hydrate Hole site. By contrast, AOM-driven hydrate dissolution as a consequence of an overall net decrease in upward methane flux seems to have persisted for a considerably longer time at the Worm Hole site, amounting to a few tens of thousands of years.