Return to search

Deciding difference logic in a Nelson-Oppen combination framework

Made available in DSpace on 2014-12-17T15:47:48Z (GMT). No. of bitstreams: 1
DiegoCBO.pdf: 564820 bytes, checksum: eedd81c1881d60fea03c3dcdd8556734 (MD5)
Previous issue date: 2007-11-07 / 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

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/17987
Date07 November 2007
CreatorsOliveira, Diego Caminha Barbosa de
ContributorsCPF:00809085437, http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5, Oliveira, Marcel Vinicius Medeiros, CPF:02386943488, http://lattes.cnpq.br/1756952696097255, Menz, Stephan, D?harbe, David Boris Paul
PublisherUniversidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Sistemas e Computa??o, UFRN, BR, Ci?ncia da Computa??o
Source SetsIBICT Brazilian ETDs
LanguageEnglish
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Formatapplication/pdf
Sourcereponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0024 seconds