• OTTER

  • Referenced in 314 articles [sw02904]
  • facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing...
  • Waldmeister

  • Referenced in 44 articles [sw19568]
  • logic. Its proof procedure is unfailing Knuth-Bendix completion [BDP89]. Waldmeister’s main advantage...
  • kbmag

  • Referenced in 19 articles [sw04845]
  • some `C’ programs for running the Knuth-Bendix completion program on finite semigroup, monoid...
  • Slothrop

  • Referenced in 10 articles [sw10019]
  • with a modern termination checker. A Knuth-Bendix completion procedure is parametrized by a reduction ... used, modern completion tools typically implement only Knuth-Bendix and path orderings. Consequently, the theories ... which completion can possibly yield a decision procedure are limited to those that ... present a variant on the Knuth-Bendix completion procedure in which no ordering is assumed...
  • DISCOUNT

  • Referenced in 14 articles [sw19613]
  • uses an extended version of unfailing Knuth-Bendix completion that is able to deal with...
  • Tyrolean

  • Referenced in 89 articles [sw07830]
  • term rewrite systems. It is the completely redesigned successor of TTT. Current (non-)termination techniques ... argument filtering, bounds, dependency pair method, Knuth-Bendix order, lexicographic path order, loop detection, matrix...
  • mkbTT

  • Referenced in 6 articles [sw10018]
  • Multi-completion with termination tools. Knuth-Bendix completion is a classical calculus in automated deduction...
  • KBCV

  • Referenced in 3 articles [sw19459]
  • KBCV -- Knuth-Bendix completion visualizer. This paper describes a tool for Knuth-Bendix completion...
  • THEOPOGLES

  • Referenced in 2 articles [sw10105]
  • polynomials and a special Knuth-Bendix procedure. THEOPOGLES is a complete theorem prover for First ... based on a special Knuth-Bendix completion procedure working on First-Order Polynomials. The method...
  • GAP

  • Referenced in 2876 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Magma

  • Referenced in 2917 articles [sw00540]
  • Computer algebra system (CAS). Magma is a large...
  • Mathematica

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

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

  • Referenced in 561 articles [sw00611]
  • graph-theoretic program NAUTY: nauty is a program...
  • PLUMP

  • Referenced in 14 articles [sw00718]
  • The joint CSCS-ETH/NEC collaboration in parallel...
  • VAMPIRE

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

  • Referenced in 851 articles [sw03521]
  • Haskell is a standardized, general-purpose purely functional...
  • TPTP

  • Referenced in 378 articles [sw04143]
  • The TPTP (Thousands of Problems for Theorem Provers...
  • Metis_

  • Referenced in 53 articles [sw04439]
  • Metis is an automatic theorem prover for first...
  • Miranda

  • Referenced in 152 articles [sw04986]
  • Miranda: A non-strict functional language with polymorphic...