TABLEAUX

TABLEAUX: A general theorem prover for modal logics. We present a general theorem proving system for propositional modal logics, called TABLEAUX. The main feature of the system is its generality, since it provides a unified environment for various kinds of modal operators and for a wide class of modal logics, including usual temporal, epistemic or dynamic logics. We survey the modal languages covered by TABLEAUX, which range from the basic one $L(square,lozenge)$ through a complex multimodal language including several families of operators with their transitive closure and converse. The decision procedure we use is basically a semantic tableaux method, but with slight modifications compared to the traditional one. We emphasize the advantages of such semantical proof methods for modal logics, since we believe that the model construction they provide represents perhaps the most attractive feature of these logics for possible applications in computer science and AI. The system has been implemented in Prolog, and appears to be of reasonable efficiency for most current examples. Experimental results are given, with two lists of test examples.