Deciding diﬀerence logic in a Nelson-Oppen combination framework - Oliveira, Diego Caminha Barbosa de (2007)
O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria especíﬁca, 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 beneﬁciados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Diﬀerence 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. Diﬀerence logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Diﬀerence logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eﬁcientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para diﬀerence logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de diﬀerence logic tem como objetivo principal informar se um conjunto de constraints de diﬀerence 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 diﬀerence 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