Prova automática de teoremas para lógicas confluentes

Abstract

Este trabalho é um projeto sobre lógicas multimodais. É apresentado o arcabouço teórico básico da sintaxe e semântica da lógica multimodal Kn e também o cálculo de resolução para Kn e suas extensões pelos axiomas confluentes: Ta, Bana, Ba, Da, 4a, G0,1,1,1 a , Fa, 5a e G1a, onde a refere-se ao índice do agente. A parte de experimentação do trabalho consistiu de dois experimentos com o provador KSP. O primeiro experimento consistiu na verificação da correção da implementação das regras de inferência de confluência, onde foram feitos testes de coerência interna nas regras oriundas de um mesmo axioma. Foi identificada falha para a regra de inferência relacionada a um axioma. O segundo experimento consistiu na refatoração do código tendo como objetivo a melhoria de desempenho por meio da mudança de estruturas de dados na parte do pré-processamento. De maneira geral o novo desempenho do programa é pior, porque soluciona menos fórmulas que a implementação antiga. Porém o resultado foi bastante heterogêneo. Apesar da implementação antiga solucionar mais fórmulas, os tempos de resolução foram muito parecidos. Seis regras de inferência tiveram tempo melhor na nova implementação e sete tiveram um tempo pior.