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.
julho 17, 2013, 15:0
Publicação
Obra sujeita a Direitos de Autor
Orientação
