• LoTREC

  • Referenced in 25 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...
  • MuPAD-Combinat

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

  • Referenced in 11 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, (non-commutative) 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 5 articles [sw13308]
  • automated theorem prover based on higher-order tableaux. HOT is an automated higher-order theorem ... based on ℋ𝒯ℰ an extensional higher-order tableaux calculus. The first part of this paper...
  • evt

  • Referenced in 7 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 proof-of-concept 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 (one-step) 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 tableaux-based 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 tableaux-based 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) hyper-resolution 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...
  • R-SATCHMO

  • Referenced in 3 articles [sw06620]
  • formalized as positive unit hyperresolution tableaux, to pruning away redundant branches. However, I-SATCHMO does...
  • pdl-tableau

  • Referenced in 2 articles [sw11994]
  • Combining Deduction and Model Checking into Tableaux and Algorithms for Converse-PDL” (Information and Computation...
  • MODPROF

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