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

Em direção a uma representação para equações algébricas :uma lógica equacional local

The intervalar arithmetic well-known as arithmetic of Moore, doesn't possess the same properties of the real numbers, and for this reason, it is confronted with a problem of operative nature, when we want to solve intervalar equations as extension of real equations by the usual equality and of the intervalar arithmetic, for this not to possess the inverse addictive, as well as, the property of the distributivity of the multiplication for the sum doesn t be valid for any triplet of intervals. The lack of those properties disables the use of equacional logic, so much for the resolution of an intervalar equation using the same, as for a representation of a real equation, and still, for the algebraic verification of properties of a computational system, whose data are real numbers represented by intervals. However, with the notion of order of information and of approach on intervals, introduced by Acióly[6] in 1991, the idea of an intervalar equation appears to represent a real equation satisfactorily, since the terms of the intervalar equation carry the information about the solution of the real equation. In 1999, Santiago proposed the notion of simple equality and, later on, local equality for intervals [8] and [33]. Based on that idea, this dissertation extends Santiago's local groups for local algebras, following the idea of Σ-algebras according to (Hennessy[31], 1988) and (Santiago[7], 1995). One of the contributions of this dissertation, is the theorem 5.1.3.2 that it guarantees that, when deducing a local Σ-equation E t t in the proposed system SDedLoc(E), the interpretations of t and t' will be locally the same in any local Σ-algebra that satisfies the group of fixed equations local E, whenever t and t have meaning in A. This assures to a kind of safety between the local equacional logic and the local algebras

Especificação do tipo intervalar parametrizado em CASL

The interval datatype applications in several areas is important to construct a interval type reusable, i.e., a interval constructor can be applied to any datatype and get intervals this datatype. Since the interval is, of certain form, a set of elements limited for two bounds, left and right, with a order notions, then it s reasonable that interval constructor enclose datatypes with partial order. On the order hand, what we want is work with interval of any datatype like this we work with this datatype then. it s important to guarantee the properties of the datatype when maps to interval of this datatype. Thus, the interval constructor get a theory to parametrized interval type, i.e., a interval with generics parameters (for example rational, real, complex). Sometimes, the interval application in some algebras doesn t guarantee the mainutenance of their properties, for example, when we use interval of real, that satisfies the field properties, it doesn t guarantee the distributivity propertie. A form to surpass this problem Santiago introduced the local equality theory that weakened the notion of strong equality, and thus, allowing some properties are local keeped, what can be discard before. The interval arithmetic generalization aim to apply the interval constructor on ordered algebras weakened for local equality with the purpose of the keep their properties. How the intervals are important in applications with continuous data, it s interesting specify that theory using a specification language that supply a system development using intervals of form disciplined, trustworth and safe. Currently, the algebraic specification language, based in math models, have been use to that intention often. We choose CASL (Common Algebraic Specification Language) among others languages because CASL has several characteristics excellent to parametrized interval type, such as, provide parcialiy and parametrization

Alterações dos parâmetros climáticos no município de Apodi-RN, antes e após a construção da barragem Santa Cruz do Apodi, e formação do lago

Este trabalho teve como objetivo principal analisar as mudanças ocorridas no clima local onde o município de Apodi/RN está inserido, em virtude da construção da Barragem Santa Cruz do Apodi. Foram utilizadas para o tratamento dos dados climáticos precipitação pluviométrica, umidade relativa do ar e temperatura técnicas estatísticas como Desvio Padrão, Teste T, Coeficiente de Variação e Média aritmética, além do modelo matemático. Para o balanço hídrico foi aplicado o método de Thornthwait (1948), considerando dois períodos em análise: o anterior e posterior a construção da Barragem Santa Cruz do Apodi, respectivamente 1995 e 2005. os resultados obtidos permitiram inferir que a hipótese inicial levantada se confirma, ou seja, a construção da Barragem Santa Cruz do Apodi, está influenciando diretamente numa alteração no que concerne à condição atmosférica local, especialmente no parâmetro umidade relativa do ar. Quanto ao balanço hídrico, observou-se a predominância do déficit hídrico especialmente entre os meses de junho a janeiro, período de estiagem; um excedente ocorrente entre os meses de maio e junho, conseqüente do período chuvoso; e uma reposição hídrica antecedendo e sucedendo este período, chuvoso, ou seja, compreendendo os meses de fevereiro a junho. Todas as considerações e análises poderão contribuir para o planejamento de abastecimento d´água, a irrigação, auxílio na previsão de enchentes e estiagens, bem como o manejo do uso da água subterrânea

Metodologia para estudo do volume e densidade absoluta da placenta humana de termo

OBJETIVO: comparar duas metodologias para o cálculo do volume placentário em gestações normais de termo: a do princípio de Arquimedes e a do volume do cilindro, para estimar a densidade absoluta da placenta. Definir a metodologia mais adequada para o cálculo do volume e densidade placentários, que se relacione com o peso e classificação do recém-nascido. MÉTODOS: foram estudadas 50 placentas provenientes de gestações de termo sem complicações e calculados o volume e a densidade absoluta placentários: a) pelo princípio de Arquimedes e b) na suposição de que a placenta seria uma secção de cilindro com duas alturas diferentes do bolo placentário: com a altura média e com a altura da média aritmética do centro e extremidades. As densidades absolutas placentárias foram calculadas pelo quociente entre o peso ao ar da placenta e os diferentes volumes. RESULTADOS: a maioria das gestantes eram multíparas, idade média de 25,4 anos, volume placentário médio entre 547,8 e 610 cm³ e densidade média entre 0,94 e 1,14 g/cm³, dependendo da metodologia empregada. CONCLUSÕES: a metodologia mais adequada para estimar o volume placentário no termo foi a do princípio de Arquimedes, pela melhor correlação com o peso dos recém-nascidos, o índice placentário e a classificação do peso dos recém-nascidos em relação à idade gestacional.

Determination and padronization of normal values of bone mineral density (BMD) of the acessory carpus bone in young Thoroughbred horse using optical densitometry in radiographic image

Em 12 fêmeas e 12 machos da raça Puro Sangue Inglês com idade média de 12 meses, avaliou-se os valores normais da densidade mineral óssea do carpo acessório em milímetros de alumínio (mmAl) até o momento do fechamento completo da epífise distal do rádio, por meio do método de densitometria óptica em imagens radiográficas. A avaliação foi realizada por meio de um programa computacional (software) especialmente desenvolvido para medida de densidade óptica em filmes de raios-X, o qual contém a imagem radiográfica do osso carpo acessório, região de partes moles adjacente ao carpo acessório e os degraus de uma escala de alumínio (phatom), que permitiu a medida de densidade mineral óssea, sendo esta a média aritmética da região de interesse determinada no osso carpo acessório correspondente ao valor em milímetros da escala. Os valores da densidade mineral óssea em mmAl do acessório do carpo em função da idade não apresentaram diferenças entre os sexos (p=0,86) permitindo que uma equação de reta fosse ajustada para ambos os sexos (densidade mineral óssea (DMO) mmAl = 3.109 + 0,056 x idade em meses), na faixa etária estudada.

Discalculia do desenvolvimento: avaliação da representação numérica pela ZAREKI-R

O presente estudo investigou aspectos da representação numérica (processamento numérico e cálculo) e memória operacional de crianças com transtornos de aprendizagem. Participaram 30 crianças de idade entre 9 e 10 anos, ambos os gêneros, divididas em dois grupos: sem dificuldade em aritmética (SDA; N=11) e com dificuldade em aritmética (CDA; N=19), avaliadas pela ZAREKI-R, Matrizes Coloridas de Raven, o Blocos de Corsi e o BCPR. Crianças CDA exibiram escores levemente mais baixos que as SDA quanto ao nível intelectual e nos Blocos de Corsi. Na ZAREKI-R apresentaram prejuízo nos subtestes ditado de números, cálculo mental, problemas aritméticos e total. Crianças CDA apresentaram déficits específicos em memória operacional visuoespacial e comprometimento em processamento numérico e cálculo, compatível com discalculia do desenvolvimento.

Utilização de redes neurais artificiais para a determinação do número de refeições diárias de um restaurante universitário

OBJETIVO: Construir uma rede neural artificial para auxiliar os gestores de restaurantes universitários na previsão de refeições diárias. MÉTODOS: O estudo foi desenvolvido a partir do levantamento de oito variáveis que influenciam o número de refeições diárias servidas no restaurante universitário. Utiliza-se o algoritmo de treinamento Backpropagation. Os resultados por meio da rede são comparados com os da série estudada e com resultados da estimação por média aritmética simples. RESULTADOS: A rede proposta acompanha as inúmeras alterações que ocorrem no número de refeições diárias do restaurante universitário. em 73% dos dias analisados, o método das redes neurais artificiais apresenta uma taxa de acerto maior do que o método da média aritmética simples. CONCLUSÃO: A rede neural artificial mostrou-se mais adequada para a previsão do número de refeições do que a metodologia de média simples ou quando a decisão do número de refeições é feita de forma subjetiva, sem critérios científicos.

Avaliação de modelos neurais aplicados na estimação de parâmetros da retificação de cerâmicas avançadas

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Desenvolvimento de sistema de aquisição e processamento para aplicações em qualidade de energia

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Caracterização da resistência a anti-helmíntico de isolados de Haemonchus contortus e trichostrongylus colubriformis orieundo de ovinos

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Explorando vertentes matemáticas nos códigos de barras

Pós-graduação em Matemática em Rede Nacional - IBILCE

Ocorrência de anticorpos anti-Neospora caninum em rebanhos bovinos leiteiros e de corte da região de Presidente Prudente-SP

Pós-graduação em Medicina Veterinária - FMVZ

Explorando conexões entre a matemática e a física com o uso da calculadora gráfica e do CBL

Pós-graduação em Educação Matemática - IGCE

A noção de função em Frege

Pós-graduação em Educação Matemática - IGCE