Deciding Kleene Algebra Terms Equivalence in Coq

This paper presents a mechanically verified implementation of an algorithm for deciding the equivalence of Kleene algebra terms within the Coq proof assistant. The algorithm decides equivalence of two given regular expressions through an iterated process of testing the equivalence of their partial derivatives and does not require the construction of the corresponding automata. Recent theoretical and experimental research provides evidence that this method is, on average, more efficient than the classical methods based on automata. We present some performance tests, comparisons with similar approaches, and also introduce a generalization of the algorithm to decide the equivalence of terms of Kleene algebra with tests. The motivation for the work presented in this paper is that of using the libraries developed as trusted frameworks for carrying out certified program verification.

Localização da página web da VisionSpace – do inglês ao francês

Trabalho de Projeto apresentado ao Instituto de Contabilidade e Administração do Porto para a obtenção do grau de Mestre em Tradução e Interpretação Especializadas, sob orientação do Doutor Manuel Moreira da Silva e coorientação da Mestre Isabelle Tulekian

Seasonal patterns of polycyclic aromatic hydrocarbons in digestive gland and arm of octopus (Octopus vulgaris) from the Northwest Atlantic

Among organic pollutants existing in coastal areas, polycyclic aromatic hydrocarbons (PAHs) are of great concern due to their ubiquity and carcinogenic potential. The aim of this study was to evaluate the seasonal patterns of PAHs in the digestive gland and arm of the common octopus (Octopus vulgaris) from the Northwest Atlantic Portuguese coast. In the different seasons, 18 PAHs were determined and the detoxification capacity of the species was evaluated. Ethoxyresorufin O-deethylase (EROD) and ethoxycoumarin O-deethylase (ECOD) activities were measured to assess phase I biotransformation capacity. Individual PAH ratios were used for major source (pyrolytic/petrogenic) analysis. Risks for human consumption were determined by the total toxicity equivalence approach. Generally, low levels of PAHs were detected in the digestive gland and in the arm of octopus, with a predominance of low molecular over high molecular weight compounds. PAHs exhibited seasonality in the concentrations detected and in their main emission sources. In the digestive gland, the highest total PAH levels were observed in autumn possibly related to fat availability in the ecosystem and food intake. The lack of PAH elimination observed in the digestive gland after captivity could be possibly associated to a low biotransformation capacity, consistent with the negligible/undetected levels of EROD and ECOD activity in the different seasons. The emission sources of PAHs found in the digestive gland varied from a petrogenic profile observed in winter to a pyrolytic pattern in spring. In the arm, the highest PAH contents were observed in June; nevertheless, levels were always below the regulatory limits established for food consumption. The carcinogenic potential calculated for all the sampling periods in the arm were markedly lower than the ones found in various aquatic species from different marine environments. The results presented in this study give relevant baseline data for environmental monitoring of organic pollution in coastal areas.

Localização de ontologias - elementos para a construção de uma abordagem

O desenvolvimento de recursos multilingues robustos para fazer face às exigências crescentes na complexidade dos processos intra e inter-organizacionais é um processo complexo que obriga a um aumento da qualidade nos modos de interacção e partilha dos recursos das organizações, através, por exemplo, de um maior envolvimento dos diferentes interlocutores em formas eficazes e inovadoras de colaboração. É um processo em que se identificam vários problemas e dificuldades, como sendo, no caso da criação de bases de dados lexicais multilingues, o desenvolvimento de uma arquitectura capaz de dar resposta a um conjunto vasto de questões linguísticas, como a polissemia, os padrões lexicais ou os equivalentes de tradução. Estas questões colocam-se na construção quer dos recursos terminológicos, quer de ontologias multilingues. No caso da construção de uma ontologia em diferentes línguas, processo no qual focalizaremos a nossa atenção, as questões e a complexidade aumentam, dado o tipo e propósitos do artefacto semântico, os elementos a localizar (conceitos e relações conceptuais) e o contexto em que o processo de localização ocorre. Pretendemos, assim, com este artigo, analisar o conceito e o processo de localização no contexto dos sistemas de gestão do conhecimento baseados em ontologias, tendo em atenção o papel central da terminologia no processo de localização, as diferentes abordagens e modelos propostos, bem como as ferramentas de base linguística que apoiam a implementação do processo. Procuraremos, finalmente, estabelecer alguns paralelismos entre o processo tradicional de localização e o processo de localização de ontologias, para melhor o situar e definir.