Results 1 to 20 of 75
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 27 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 1890 articles [sw00161]
  • Coq is a formal proof management system. It...

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

  • Maple
  • Referenced in 5373 articles [sw00545]
  • The result of over 30 years of cutting...

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

  • MiniSat
  • Referenced in 566 articles [sw00577]
  • An extensible SAT-solver. MiniSat is a minimalistic...

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

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

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

  • SOLAR
  • Referenced in 20 articles [sw00888]
  • SOLAR (SOL for Advanced Reasoning) is a first...

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

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

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