Implementação da combinação de métodos de prova automática de teoremas para lógicas modais

Abstract

Este trabalho apresenta as modificações feitas no KSP, um provador de teoremas baseado em resolução para a Lógica Multimodal Kn, para permitir que o provador também lide com a combinação dos raciocínios local e global. Para o completo entendimento do leitor, a sintaxe e semântica da Lógica Multimodal Kn são descritas, assim como o cálculo utilizado no KSP e sua implementação. Uma avaliação experimental foi executada durante o desenvolvimento deste projeto para garantir que a performance do provador não sofresse alteração significativa, que o provador continuasse lidando com os raciocínios local e global corretamente e que a implementação da combinação dos dois raciocínios resultasse em concordância com o cálculo. Os resultados obtidos mostram que o tempo de execução para os cálculos local e global separadamente foi semelhante antes e após as modificações do provador para o mesmo conjunto de testes. Também foi possível concluir que as saídas sobre a satisfatibilidade foram iguais às esperadas para este conjunto de testes. Em relação aos testes executados para a combinação dos dois cálculos, parte do conjunto de cláusulas cumpriram a expectativa porém um dos testes apresentou erros. Por isso, a refatoração do provador e uma nova experimentação são necessárias.