• SATCHMO

  • Referenced in 97 articles [sw06619]
  • small Prolog-program, which implements a tableau proof procedure. One restriction is that it requires...
  • KL-ONE

  • Referenced in 41 articles [sw28891]
  • overview of tableau algorithms for description logics. Description logics are a family of knowledge representation ... description logics can be decided using tableau-like algorithms. This is not very surprising since ... such as propositional dynamic logic), for which tableau procedures have been quite successful. Nevertheless ... program logics. Consequently, the research on tableau algorithms in description logics led to new techniques...
  • Racer

  • Referenced in 66 articles [sw09837]
  • representation system that implements a highly optimized tableau calculus for the description logic SRIQ...
  • Satallax

  • Referenced in 55 articles [sw06849]
  • clauses corresponding to rules of a complete tableau calculus and calls MiniSat periodically to test...
  • leanCoP

  • Referenced in 31 articles [sw09756]
  • first-order logic, based on the connection (tableau) calculus and implemented in Prolog. leanCoP...
  • ModLeanTAP

  • Referenced in 19 articles [sw12368]
  • ModLeanTAP: Lean Tableau-based Deduction for Propositional Modal Logics. ModLeanTAP is a lean Prolog implementation ... modular labelled tableau calculus for propositional modal logics (where the labels contain free and universal ... development was inspired by the lean tableau-based prover for first-order logic leanTAP. ModLeanTAP...
  • MetTeL

  • Referenced in 16 articles [sw11990]
  • MetTeL: A tableau prover with logic-independent inference engine. MetTeL is a generic tableau prover ... component of MetTeL is a logic-independent tableau inference engine. A novel feature is that ... ability to flexibly specify the set of tableau rules to be used in derivations. Termination...
  • SOLAR

  • Referenced in 20 articles [sw00888]
  • based on the SOL (Skip Ordered Linear) tableau calculus. The ability to find non-trivial ... nonmonotonic reasoning. SOL is a connection tableau calculus which is complete for finding...
  • LoTREC

  • Referenced in 27 articles [sw07684]
  • characterized by a high-level language for tableau rules and strategies. It aims at covering...
  • Zenon

  • Referenced in 23 articles [sw06753]
  • classical logic (with equality), based on the tableau method. Zenon is intended...
  • MaLeCoP

  • Referenced in 23 articles [sw07197]
  • learned knowledge is added to the connection tableau calculus and implemented...
  • HARP

  • Referenced in 16 articles [sw26323]
  • HARP: A tableau-based theorem prover. This paper presents HARP, a complete, tableau-based theorem...
  • Spartacus

  • Referenced in 15 articles [sw12426]
  • Spartacus: A Tableau Prover for Hybrid Logic. Spartacus is a tableau prover for hybrid multimodal...
  • TTM

  • Referenced in 12 articles [sw11997]
  • Tableau-based Theorem Prover for Temporal Logic PLTL. TTM is a theorem prover ... based on a one-pass tableau method for PLTL called the context-based tableau method...
  • E-KRHyper

  • Referenced in 13 articles [sw21368]
  • equality. It implements the new E-hyper tableau calculus, which integrates a superposition-based handling ... equality into the hyper tableau calculus. E-KRHyper extends our previous KRHyper system, which...
  • FEMaLeCoP

  • Referenced in 15 articles [sw21179]
  • learning connection prover. FEMaLeCoP is a connection tableau theorem prover based on leanCoP which uses...
  • 3TAP

  • Referenced in 13 articles [sw21544]
  • Tableau-Based Theorem Prover 3TAP for Multiple-Valued Logics...
  • linTAP

  • Referenced in 7 articles [sw11991]
  • linTAP is a tableau prover for the multiplicative and exponential fragment of Girards linear logic ... given formula by constructing an analytic tableau and ensures the linear validity using prefix unification ... linear logic. Based on a prefixed semantic tableau calculus. Sound and complete. Source code available...
  • TATL

  • Referenced in 7 articles [sw07522]
  • TATL: implementation of ATL tableau-based decision procedure. This paper describes the implementation ... tableau-based decision procedure for the alternating-time temporal logic proposed by Goranko and Shkatov...
  • MAVEN

  • Referenced in 10 articles [sw07659]
  • state machine of the aspect advice. The tableau of the LTL assumption is used...