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

Excitações elementares em super-redes quasiperiódicas com simetria espelho

In this thesis, we investigated the magnonic and photonic structures that exhibit the so-called deterministic disorder. Speci cally, we studied the effects of the quasiperiodicity, associated with an internal structural symmetry, called mirror symmetry, on the spectra of photonics and magnonics multilayer. The quasiperiodicity is introduced when stacked layers following the so-called substitutional sequences. The three sequences used here were the Fibonacci sequence, Thue-Morse and double-period, all with mirror symmetry. Aiming to study the propagation of light waves in multilayer photonic, and spin waves propagation in multilayer magnonic, we use a theoretical model based on transfer matrix treatment. For the propagation of light waves, we present numerical results that show that the quasiperiodicity associated with a mirror symmetry greatly increases the intensity of transmission and the transmission spectra exhibit a pro le self-similar. The return map plotted for this system show that the presence of internal symmetry does not alter the pattern of Fibonacci maps when compared with the case without symmetry. But when comparing the maps of Thue-Morse and double-time sequences with their case without the symmetry mirror, is evident the change in the pro le of the maps. For magnetic multilayers, we work with two di erent systems, multilayer composed of a metamagnetic material and a non-magnetic material, and multilayers composed of two cubic Heisenberg ferromagnets. In the rst case, our calculations are carried out in the magnetostatic regime and calculate the dispersion relation of spin waves for the metamgnetic material considered FeBr2. We show the e ect of mirror symmetry in the spectra of spin waves, and made the analysis of the location of bulk bands and the scaling laws between the full width of the bands allowed and the number of layers of unit cell. Finally, we calculate the transmission spectra of spin waves in quasiperiodic multilayers consisting of Heisenberg ferromagnets. The transmission spectra exhibit self-similar patterns, with regions of scaling well-de ned in frequency and the return maps indicates only dependence of the particular sequence used in the construction of the multilayer