An automatic theorem prover for a proof system in the style of dual tableaux for the relational logic associated with modal logic K has been introduced. Although there are many well-known implementations
of provers for modal logic, as far as we know, it is the first implementation of a specific relational prover for a standard modal logic. There are two main contributions in this paper. First, the implementation of new rules, called (k1) and (k2), which substitute the classical relational rules …
Read moreAn automatic theorem prover for a proof system in the style of dual tableaux for the relational logic associated with modal logic K has been introduced. Although there are many well-known implementations
of provers for modal logic, as far as we know, it is the first implementation of a specific relational prover for a standard modal logic. There are two main contributions in this paper. First, the implementation of new rules, called (k1) and (k2), which substitute the classical relational rules for composition and negation of composition in order to guarantee not only that every proof tree is finite but also to decrease the number of applied rules in dual tableaux. Second, the implementation of an order of application of the rules which ensures that the proof tree obtained is unique.As a consequence, we have implemented a decision procedure for modal logic K. Moreover, this work would be the basis for successive extensions of this logic, such as
T, B and S4.
