
LoTREC
 Referenced in 27 articles
[sw07684]
 LoTREC: Logical tableaux research engineering companion. In this paper we describe a generic tableaux system ... learning system for possible worlds semantics and tableaux based proof methods...

TABLEAUX
 Referenced in 18 articles
[sw11674]
 TABLEAUX: A general theorem prover for modal logics. We present a general theorem proving system ... propositional modal logics, called TABLEAUX. The main feature of the system is its generality, since ... survey the modal languages covered by TABLEAUX, which range from the basic one $L(square ... procedure we use is basically a semantic tableaux method, but with slight modifications compared...

MuPADCombinat
 Referenced in 25 articles
[sw04933]
 deal with most usual combinatorial classes (partitions, tableaux, decomposable classes, ...). It also supplies the user...

HTab
 Referenced in 12 articles
[sw12427]
 HTab: a Terminating Tableaux System for Hybrid Logic. Hybrid logic is a formalism that ... method. An alternative to resolution is the tableaux method, already widely used for both modal ... description logics. Tableaux algorithms have also been developed for a number of hybrid logics ... present the implementation of a terminating tableaux algorithm for the hybrid logic...

ACE
 Referenced in 13 articles
[sw15066]
 objects as partitions, compositions, permutations, words, Young tableaux, divided differences, (noncommutative) symmetric functions...

AdinKingRoichman
 Referenced in 10 articles
[sw11417]
 fascinating article ”Enumeration of standard Young tableaux of certain truncated shapes” by Ron Adin, Ronald...

HOT
 Referenced in 6 articles
[sw13308]
 automated theorem prover based on higherorder tableaux. HOT is an automated higherorder theorem ... based on ℋ𝒯ℰ an extensional higherorder tableaux calculus. The first part of this paper...

evt
 Referenced in 8 articles
[sw09805]
 graphical interface permits easy navigation through proof tableaux, proof reuse, and meaningful feedback about...

HyLoTab
 Referenced in 7 articles
[sw13662]
 HyLoTab is a proofofconcept tableaux prover for hybrid logics originally written...

PERMS
 Referenced in 7 articles
[sw20247]
 permutation groups; Group ring tools; Partitions, types, tableaux; Special idempotents and generating elements; Characters, Littlewood...

Cool
 Referenced in 4 articles
[sw11992]
 core of Cool is an efficient unlabelled tableaux search procedure using global caching. Concrete logics ... added by implemening the corresponding (onestep) tableaux rules. The logics covered at the moment...

PreDeLo
 Referenced in 3 articles
[sw13719]
 Prolog implementation of labelled tableaux calculi for such extensions, and it is able to deal ... that each axiom or rule of the tableaux calculi is implemented by a Prolog clause ... this paper, we also introduce a tableaux calculus for checking entailment in the rational extension...

CSLLean
 Referenced in 4 articles
[sw09984]
 direct Prolog implementation of a tableauxbased decision procedure recently proposed for this logic...

KLMLean
 Referenced in 4 articles
[sw09988]
 nonmonotonic reasoning. KLMLean 2.0 implements some analytic tableaux calculi for these logics recently introduced. KLMLean...

MoMo
 Referenced in 4 articles
[sw10020]
 equipped with a sound and complete tableauxbased proof system...

TWB
 Referenced in 4 articles
[sw17666]
 changed substantially since our system description in TABLEAUX...

Sofia
 Referenced in 1 article
[sw30125]
 HyperS tableaux  heuristic hyper tableaux. Several syntactic methods have been constructed to automate theorem proving ... positive (negative) hyperresolution and the clause tableaux were combined in a single calculus called ... hyper tableaux. In this paper we propose a new calculus, called hyperS tableaux, which overcomes ... substantial drawbacks of hyper tableaux. In contrast to hyper tableaux, hyperS tableaux are entirely automated...

RSATCHMO
 Referenced in 3 articles
[sw06620]
 formalized as positive unit hyperresolution tableaux, to pruning away redundant branches. However, ISATCHMO does...

pdltableau
 Referenced in 2 articles
[sw11994]
 Combining Deduction and Model Checking into Tableaux and Algorithms for ConversePDL” (Information and Computation...

MODPROF
 Referenced in 2 articles
[sw21543]
 MODPROF is based on labelled modal tableaux. Its novel feature is a sophisticated simplification algorithm...