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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/17987 |
| Date | 07 November 2007 |
| Creators | Oliveira, Diego Caminha Barbosa de |
| Contributors | CPF: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 |
| Publisher | Universidade 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 Sets | IBICT Brazilian ETDs |
| Language | English |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0019 seconds