Implementation of a Matrix Theorem Prover for Propositional Modal Logic

摘要

The implementation of a matrix theorem prover for the propositional modal logicS5 is presented. A matrix theorem prover for classical logic is adapted to perform semantic tableaux-based proofs in the modal logic S5 by means of exploring the peculiar accessibility relation defined by the possible-worlds semantics for this logic. This method is easily adaptable to execute proofs in other modal logics. The relevant literature is surveyed and the proof method is presented in detail along with its implementation. The adaptation of the program to work for other logics is discussed.