Dissertação

On Nelson-Oppen techniques EVALUATED

O método de Nelson-Oppen permite a combinação modular de procedimentos de satisfação de fórmulas sem quantificadores em teorias de primeira ordem num procedimento de satisfação de fórmulas sem quantificadores para a união das teorias. Este método, no entanto, requer que as teorias a unir tenham assinaturas disjuntas e que sejam estavelmente infinitas. Dada a importância do método, várias propostas com vista à extensão do método para outras classes de teorias foram feitas. Recentemente, duas extensões do método de Nelson-Oppen foram feitas, substituindo o requisito de que as teorias a unir tenham de ser estavelmente infinitas: uma envolvendo teorias shiny e a outra teorias polite. As relações entre teorias shiny e teorias polite são também analisadas. Mais tarde, uma noção mais forte de teorias polite foi proposta, de modo a superar um pormenor técnico na demonstração da correcção do método de Nelson-Oppen para teorias polite. Nesta tese, descrevemos o método original de Nelson e Oppen, assim como as suas extensões a teorias shiny, polite e fortemente polite. Respondendo a uma questão deixada em aberto, analisamos as relações entre teorias shiny e fortemente polite. Mostramos que uma teoria shiny com o problema de satisfação de fórmulas sem quantificadores decidível é fortemente polite e provamos que sob dois conjuntos de hipóteses, uma teoria fortemente polite é shiny.
combinação de procedimentos de satisfação, método de Nelson-Oppen, teorias polite, teorias fortemente polite, teorias shiny

Julho 17, 2013, 15:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

João Filipe Quintas dos Santos Rasga

Departamento de Matemática (DM)

Professor Auxiliar