• TABLEAUX

  • Referenced in 18 articles [sw11674]
  • 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 ... emphasize the advantages of such semantical proof methods for modal logics, since we believe that...
  • LoTREC

  • Referenced in 25 articles [sw07684]
  • this paper we describe a generic tableaux system for building models or counter-models ... strategies. It aims at covering all Kripke-semantic based logics. It is implemented in Java ... learning system for possible worlds semantics and tableaux based proof methods...
  • DARR

  • Referenced in 1 article [sw25431]
  • default logics. A modified version of semantic tableaux method is used to implement the propositional...
  • Molle

  • Referenced in 0 articles [sw05747]
  • modal logic. It exploits the modal semantic tableaux method. It features a very usable graphical...
  • Cool

  • Referenced in 4 articles [sw11992]
  • beyond relational semantics. The core of Cool is an efficient unlabelled tableaux search procedure using...
  • PreDeLo

  • Referenced in 3 articles [sw13719]
  • preferential semantics. PreDeLo 1.0 is a Prolog implementation of labelled tableaux calculi for such extensions...
  • DysToPic

  • Referenced in 1 article [sw31857]
  • semantics. DysToPic is a multi-engine Prolog implementation of a labelled, two-phase tableaux calculus...
  • Coq

  • Referenced in 1818 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Isabelle

  • Referenced in 617 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • Maple

  • Referenced in 5168 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 6041 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • MuPAD

  • Referenced in 138 articles [sw00606]
  • MuPAD consists of a powerful symbolic engine, a...
  • SETHEO

  • Referenced in 119 articles [sw00707]
  • SETHEO: A high-performance theorem prover. The paper...
  • SageMath

  • Referenced in 1714 articles [sw00825]
  • Sage (SageMath) is free, open-source math software...
  • TPS

  • Referenced in 71 articles [sw00973]
  • TPS and ETPS are, respectively, the Theorem Proving...
  • GOLOG

  • Referenced in 170 articles [sw02159]
  • GOLOG: A logic programming language for dynamic domains...
  • OTTER

  • Referenced in 315 articles [sw02904]
  • Our current automated deduction system Otter is designed...
  • VAMPIRE

  • Referenced in 239 articles [sw02918]
  • Vampire 8.0, [RV02,Vor05] is an automatic theorem...
  • PVS

  • Referenced in 624 articles [sw03484]
  • PVS is a verification system: that is, a...