×

TABLEAUX

swMATH ID: 11674
Software Authors: Catach, Laurent
Description: 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.
Homepage: http://rd.springer.com/article/10.1007%2FBF01880326
Keywords: experimental results; temporal logic; dynamic logic; epistemic logic; general theorem proving system; propositional modal logics; multimodal language; decision procedure; semantic tableaux; Prolog; test examples
Related Software: Pesca; KRIPKE; SPASS; LoTREC; MOIN; LWB; HARP; GLEFatinf; KQML; GQML; GULP; OTTER; PRIZ; Coq; Imogen; IntHistGC; ileanCoP; STRIP; ILTP; QMLTP
Cited in: 21 Documents

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
TABLEAUX: A general theorem prover for modal logics. Zbl 0743.03008
Catach, Laurent
1991
all top 5

Cited by 32 Authors

2 de Nivelle, Hans
2 Demri, Stéphane P.
2 Dixon, Clare
2 Massacci, Fabio
2 Negri, Sara
1 Aitken, J. Stuart
1 Cantone, Domenico
1 Catach, Laurent
1 Cunningham, Jim
1 Donini, Francesco M.
1 Dyckhoff, Roy
1 Fisher, Michael
1 Girlando, Marianna
1 Giunchiglia, Fausto
1 Heuerding, Alain
1 Hustadt, Ullrich
1 Indrzejczak, Andrzej
1 Nalon, Cláudia
1 Nardi, Daniele
1 Nicolosi Asmundo, Marianna
1 Ognjanović, Zoran
1 Palm, Adi
1 Papacchini, Fabio
1 Pitt, Jeremy
1 Reichgelt, Han
1 Rosati, Riccardo
1 Roveri, Marco
1 Schwendimann, Stefan
1 Sebastiani, Roberto
1 Shadbolt, Nigel
1 Straßburger, Lutz
1 Wooldridge, Michael J.

Cited in 5 Serials

3 Journal of Automated Reasoning
1 Journal of Philosophical Logic
1 Theoretical Computer Science
1 The Bulletin of Symbolic Logic
1 Logica Universalis

Cited in 2 Fields

19 Mathematical logic and foundations (03-XX)
11 Computer science (68-XX)

Citations by Year