Implementação de um provador de teoremas por resolução para lógicas modais normais

Abstract

Neste trabalho apresentamos a implementação de um provador de teoremas para sistemas da lógica modal normal para múltiplos agentes, baseado na técnica de resolução modal publicada por Nalon and Dixon [2007]. Ao contrário das demais abordagens de prova por resolução na lógica modal, onde as regras de inferência são elaboradas para uso em um sistema em particular (por exemplo, K, S4, S5), o método de resolução usado como base para a implementação apresentada se concentra nas restrições impostas às relações de acessibilidade entre mundos para cada sistema modal. Portanto, temos regras de inferência específicas para sistemas seriais, reflexivos, simétricos, transitivos e euclidianos, além de um conjunto de regras de inferência válidas em toda a classe de sistemas modais normais. Desta forma, a implementação torna-se abrangente, por conseguir lidar com diversos sistemas modais através da combinação das regras de inferência mencionadas, e expansível, pois basta implementar novas regras de inferência que capturem outra restrição nas relações de acessibilidade para aumentarmos a abrangência do cálculo, sem prejudicar a correção e completude dos resultados para os sistemas que já estavam cobertos. O programa apresentado, escrito na linguagem C++, efetua o cálculo de prova para os quinze sistemas modais normais definidos pelas diferentes combinações dos axiomas Di, Ti, Bi, 4i e 5i, incluindo sistemas como K(n), D(n), T(n), B(n), S4(n) e S5(n), onde o índice (n) representa a versão multi-agente de um sistema. ________________________________________________________________________________ ABSTRACT

In this work we present an implementation of a theorem prover for multi-agent normal modal logic systems, based on the modal resolution technique published by Nalon and Dixon [2007]. Differently from other approaches for resolution proof systems or methods in modal logic, where inference rules are developed for use in a particular system e.g. K, S4 or S5, the resolution method used as a basis for the implementation presented here focuses on the restrictions imposed on the accessibility relations between worlds for each modal system. Thus, we have specific inference rules for serial, reflexive, symmetric, transitive and Euclidean systems, as well as a set of inference rules for every normal modal system. Therefore, the implementation becomes comprehensive, since it can deal with several modal systems by combination of the inference rules mentioned above; and extensible, since we only need to implement new inference rules which capture another restriction in the accessibility relations to increase the range of systems included in the calculus, without compromising the soundness and completeness of the results for modal systems already covered before. The presented program, coded in the C++ language, automatically produces proofs for the fifteen distinct normal modal systems defined by the different combinations of the axioms Di, Ti, Bi, 4i and 5i, including systems like K(n), D(n), T(n), B(n), S4(n) and S5(n), where the (n) index indicates a multi-agent version of a system.