Implementing a relational theorem prover for modal logic

Abstract

An automatic theorem prover for a proof system in the style of dual tableaux for the relational logic associated with modal logic 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 () and (), 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 . Moreover, this work would be the basis for successive extensions of this logic, such as , and .

Keywords:

• relational logic
• modal logic
• dual tableau methods
• implementation theorem provers

2000 AMS Subject Classifications :

• 03B45
• 68T15

Acknowledgements

This work is partially supported by the Spanish research projects TIN2006-15455-C03-01, TIN07-65819, and the second author is partially supported also by project P6-FQM-02049. The last author of the paper is partially supported by the Polish Ministry of Science and Higher Education grant N N206 399134 and IP2010 010170. Finally, we would like to thank the anonymous reviewers for their careful reading and very helpful comments, which have made possible this version of the paper.

Notes

The full implementation (developed in SWI-Prolog Version 5.6.33 for Windows and Mac platforms) is available from the address http://files.getdropbox.com/u/1639661/Klogicv2.zip where can be seen outputs for different formulas introduced to the prover.

In 16, an explanation of the common rules for modal logics (union, intersection, etc.) is available.

http://twb.rsise.anu.edu.au/

http://www.irit.fr/ACTIVITES/LILaC/Lotrec/