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.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Indrzejczak, Andrzej: Linear time in hypersequent framework (2016)
- Negri, Sara: Proofs and countermodels in non-classical logics (2014)
- Cantone, Domenico; Nicolosi-Asmundo, Marianna: A sound framework for $\delta$-rule variants in free-variable semantic tableaux (2007)
- Negri, Sara: Proof analysis in modal logic (2005)
- Palm, Adi: Model theoretic syntax and parsing: an application to temporal logic (2004)
- Aitken, J.Stuart; Reichgelt, Han; Shadbolt, Nigel: Resolution theorem proving in reified modal logics (1994)
- Ognjanović, Zoran: A tableau-like proof procedure for normal modal logics (1994)
- Catach, Laurent: TABLEAUX: A general theorem prover for modal logics (1991)