Results 1 to 20 of 59
Sort by:

  • 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...