
OTTER
 Referenced in 314 articles
[sw02904]
 facilities for term rewriting, term orderings, KnuthBendix completion, weighting, and strategies for directing...

Waldmeister
 Referenced in 44 articles
[sw19568]
 logic. Its proof procedure is unfailing KnuthBendix completion [BDP89]. Waldmeister’s main advantage...

kbmag
 Referenced in 19 articles
[sw04845]
 some `C’ programs for running the KnuthBendix completion program on finite semigroup, monoid...

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

DISCOUNT
 Referenced in 14 articles
[sw19613]
 uses an extended version of unfailing KnuthBendix 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, KnuthBendix order, lexicographic path order, loop detection, matrix...

mkbTT
 Referenced in 6 articles
[sw10018]
 Multicompletion with termination tools. KnuthBendix completion is a classical calculus in automated deduction...

KBCV
 Referenced in 3 articles
[sw19459]
 KBCV  KnuthBendix completion visualizer. This paper describes a tool for KnuthBendix completion...

THEOPOGLES
 Referenced in 2 articles
[sw10105]
 polynomials and a special KnuthBendix procedure. THEOPOGLES is a complete theorem prover for First ... based on a special KnuthBendix completion procedure working on FirstOrder 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 SATsolver. MiniSat is a minimalistic...

nauty
 Referenced in 561 articles
[sw00611]
 graphtheoretic program NAUTY: nauty is a program...

PLUMP
 Referenced in 14 articles
[sw00718]
 The joint CSCSETH/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, generalpurpose 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 nonstrict functional language with polymorphic...