• Darwin

  • Referenced in 25 articles [sw04175]
  • formulated in tptp or tme format, non-clausal tptp problems are clausified using the eprover...
  • E-Darvin

  • Referenced in 19 articles [sw06852]
  • problems in tptp or tme syntax. Non-clausal input is clausified using the eprover...
  • nanoCoP

  • Referenced in 4 articles [sw21547]
  • nanoCoP: a non-clausal connection prover. nanoCoP is a compact non-clausal automated theorem prover ... logic. It is based on the non-clausal connection calculus for classical logic. More details ... logic with equality. Based on the non-clausal connection calculus. Proof search on the original ... leanCoP or TPTP). Output of compact non-clausal connection proof. Available under the GNU general...
  • SATO

  • Referenced in 196 articles [sw04451]
  • SATO: A Solver for Propositional Satisfiability: The Davis...
  • SATIRE

  • Referenced in 38 articles [sw04648]
  • SATIRE: A new incremental satisfiability engine. We introduce...
  • zChaff

  • Referenced in 36 articles [sw04757]
  • zChaff is an implementation of the well known...
  • Chaff

  • Referenced in 570 articles [sw06916]
  • Chaff:engineering an efficient SAT solver. Boolean Satisfiability...
  • Quaffle

  • Referenced in 64 articles [sw07278]
  • Quaffle: Quantified Boolean Formula Evaluator with Learning Quaffle...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • Nenofex: Expanding NNF for QBF Solving. The topic...