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

Processing of highly porous titanium parts by metal injection moulding in combination with innovative plasma treatment

A combinação da Moldagem por Injeção de pós Metálicos (Metal Injection Moulding MIM) e o Método do Retentor Espacial (Space Holder Method - SHM) é uma técnica promissora para fabricação de peças porosas de titânio com porosidade bem definida como implantes biomédicos, uma vez que permite um alto grau de automatização e redução dos custos de produção em larga escala quando comparado a técnica tradicional (SHM e usinagem a verde). Contudo a aplicação desta técnica é limitada pelo fato que há o fechamento parcial da porosidade na superfície das amostras, levando ao deterioramento da fixação do implante ao osso. E além disso, até o presente momento não foi possível atingir condições de processamento estáveis quando a quantidade de retentor espacial excede 50 vol. %. Entretanto, a literatura descreve que a melhor faixa de porosidade para implantes de titânio para coluna vertebral está entre 60 - 65 vol. %. Portanto, no presente estudo, duas abordagens foram conduzidas visando a produção de amostras altamente porosas através da combinação de MIM e SHM com o valor constante de retentor espacial de 70 vol. % e uma porosidade aberta na superfície. Na primeira abordagem, a quantidade ótima de retentor espacial foi investigada, para tal foram melhorados a homogeneização do feedstock e os parâmetros de processo com o propósito de permitir a injeção do feedstock. Na segunda abordagem, tratamento por plasma foi aplicado nas amostras antes da etapa final de sinterização. Ambas rotas resultaram na melhoria da estabilidade dimensional das amostras durante a extração térmica do ligante e sinterização, permitindo a sinterização de amostras de titânio altamente porosas sem deformação da estrutura.