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.

References in zbMATH (referenced in 18 articles , 1 standard article )

Showing results 1 to 18 of 18.
Sorted by year (citations)

  1. Dyckhoff, Roy: Intuitionistic decision procedures since Gentzen (2016)
  2. Indrzejczak, Andrzej: Linear time in hypersequent framework (2016)
  3. Negri, Sara: Proofs and countermodels in non-classical logics (2014)
  4. Cantone, Domenico; Nicolosi-Asmundo, Marianna: A sound framework for (\delta)-rule variants in free-variable semantic tableaux (2007)
  5. Negri, Sara: Proof analysis in modal logic (2005)
  6. Palm, Adi: Model theoretic syntax and parsing: an application to temporal logic (2004)
  7. de Nivelle, Hans: A resolution decision procedure for the guarded fragment (1998)
  8. Giunchiglia, Fausto; Roveri, Marco; Sebastiani, Roberto: A new method for testing decision procedures in modal logics (1997)
  9. Demri, Stéphane: A simple tableau system for the logic of elsewhere (1996)
  10. Donini, Francesco M.; Massacci, Fabio; Nardi, Daniele; Rosati, Riccardo: A uniform tableaux method for nonmonotonic modal logics (1996)
  11. Fisher, Michael; Wooldridge, Michael; Dixon, Clare: A resolution-based proof method for temporal logics of knowledge and belief (1996)
  12. Pitt, Jeremy; Cunningham, Jim: Distributed modal theorem proving with KE (1996)
  13. Aitken, J. Stuart; Reichgelt, Han; Shadbolt, Nigel: Resolution theorem proving in reified modal logics (1994)
  14. Demri, S.: Efficient strategies for automated reasoning in modal logics (1994)
  15. Massacci, Fabio: Strongly analytic tableaux for normal modal logics (1994)
  16. Ognjanović, Zoran: A tableau-like proof procedure for normal modal logics (1994)
  17. de Nivelle, H.: Generic resolution in propositional modal systems (1993)
  18. Catach, Laurent: TABLEAUX: A general theorem prover for modal logics (1991)