Deciding difference logic in a Nelson-Oppen combination framework

O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria específica, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneficiados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Difference logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x − y ≤ c, onde x e y são variáveis e c é uma constante. Difference logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para difference logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic é satisfatível (as variáveis podem assumir valores que tornam o conjunto consistente) ou não. Além disso, para funcionar em um modelo de combinação baseado em Nelson-Oppen, o procedimento de decisão precisa ter outras funcionalidades, como geração de igualdade de variáveis, prova de inconsistência, premissas, etc. Este trabalho apresenta um procedimento de decisão para a teoria de difference logic dentro de uma arquitetura baseada no método de combinação de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi possível observar o seu funcionamento. Detalhes de implementação e testes experimentais são relatados

Propriedades fisicas do monocristal fe/mgo(100) e estudo da expansao termica da superficie da ag(100)

In this work we have developed a way to grow Fe/MgO(100) monocrystals by magnetron sputtering DC. We investigated the growing in a temperature range among 100 oC and 300 oC. Structural and magneto-crystalline properties were studied by different experimental techniques. Thickness and surface roughness of the films were investigated by atomic force microscopy, while magneto-crystalline properties were investigated by magneto-optical Kerr effect and ferromagnetic resonance. Our results show that as we increase the deposition temperature, the magneto-crystalline anisotropy of the films also increases, following the equation of Avrami. The best temperature value to make a film is 300 oC. As the main result, we built a base of magnetoresistence devices and as an aplication, we present measurements of Fe/Cr/Fe trilayer coupling. In a second work we investigated the temperature dependence of the first three interlayer spacings of Ag(100) surface using low energy electron diffraction. A linear expansion model of crystal surface was used and the values of Debye temperatures of the first two layers and thermal expansion coefficient were determinated. A relaxation of 1% was found for Ag(100) surface and these results are matched with faces (110) and (111) of the silver. iv

analise da dispersao de ondas de superficie na provincia borborema, Nordeste do Brasil

The Borborema Province, Northeastern Brazil, had its internal structure investigated by different geophysical methods like gravity, magnetics and seismics. Additionally, many geological studies were also carried out to define the structural domains of this province. Despite the plethora of studies, there are still many important open aspects about its evolution. Here, we study the velocity structure of S-wave in the crust using dispersion of surface waves. The dispersion of surface waves allows an estimate of the average thickness of the crust across the region between the stations. The inversion of the velocity structure was carried out using the inter-station dispersion of surface waves of Rayleigh and Love types. The teleseismic events are mainly from the edges of the South and North American plates. The period of data collection occurred between 2007 and 2010 and we selected 7 events with magnitude above 5.0 MW and up to 40 km depth. The difference between the events back-azimuths and the interstation path was not greater than 10. We also know the depth of the Moho, results from Receiver Functions (Novo Barbosa, 2008), and use those as constrains in inversion. Even using different parameterizations of models for the inversion, our results were very similar the mean profiles velocity structure of S-wave. In pairs of stations located in the Cear´a Central Domain Borborema the province, there are ranges of depths for which the velocities of S are very close. Most of the results in the profile near the Moho complicate their interpretation at that depth, coinciding with the geology of the region, where there are many shear zones. In particular, the profile that have the route Potiguar Bacia in inter-station, had low velocities in the crust. We combine these results to the results of gravimetry and magnetometry (Oliveira, 2008) and receptor function (Novo Barbosa, 2008). We finally, the first results on the behavior of the velocity structure of S-wave with depth in the Province Borborema