1912:
where X is a finite set of generators and R is a set of defining relations on X. Let X be the set of all words in X (i.e. the free monoid generated by X). Since the relations R generate an equivalence relation on X*, one can consider elements of M to be the equivalence classes of X under R. For
1989:
From the presentation of the monoid it is possible to define a rewriting system given by the relations R. If A x B is in R then either A < B in which case B → A is a rule in the rewriting system, otherwise A > B and A → B. Since < is a reduction
4852:
If Knuth–Bendix does not succeed, it will either run forever and produce successive approximations to an infinite complete system, or fail when it encounters an unorientable equation (i.e. an equation that it cannot turn into a rewrite rule). An enhanced version will not fail on unorientable
1867:
and weakly confluent, then the rewriting system is confluent. So, if we can add rules to the term rewriting system in order to force all critical pairs to be convergent while maintaining the strong normalizing property, then this will force the resultant rewriting system to be confluent.
1969:
then the order < gives a consistent method for defining minimal representatives, however computing these representatives may still not be possible. In particular, if a rewriting system is used to calculate minimal representatives then the order < should also have the property:
1964:
Although the choice of a canonical form can theoretically be made in an arbitrary fashion this approach is generally not computable. (Consider that an equivalence relation on a language can produce an infinite number of infinite classes.) If the language is
2006:
of W. However, if the rewriting system given by the relations is converted to a confluent rewriting system via the Knuth–Bendix algorithm, then all reductions are guaranteed to produce the same irreducible word, namely the normal form for that word.
4723:
4868:
discussed in the paper by
Heyworth and Wensley listed below allows some recording or logging of the rewriting process as it proceeds. This is useful for computing identities among relations for presentations of groups.
3241:
3073:
1358:, computes a completion of the (additive) group axioms as in Knuth, Bendix (1970). It starts with the three initial equations for the group (neutral element 0, inverse elements, associativity), using
4842:
4784:
4520:
4450:
4259:
4082:
1910:
2048:
3896:
3730:
2280:
3401:
4380:
4329:
3341:
3290:
1990:
order a given word W can be reduced W > W_1 > ... > W_n where W_n is irreducible under the rewriting system. However, depending on the rules that are applied at each W
4539:
Checking the overlaps of these rules, we find no potential failures of confluence. Therefore, we have a confluent rewriting system, and the algorithm terminates successfully.
4202:
4025:
3522:
3001:
2240:
3846:
3680:
2961:
2323:
2180:
3789:
3564:
4998:
V. Diekert; A.J. Duncan; A.G. Myasnikov (2011). "Geodesic
Rewriting Systems and Pregroups". In Oleg Bogopolski; Inna Bumagin; Olga Kharlampovich; Enric Ventura (eds.).
4138:
3961:
2804:
2765:
5358:
2636:
2600:
2564:
2528:
2837:
2726:
4557:
3635:
3602:
3445:
2921:
2894:
2693:
2666:
2492:
2465:
2434:
2407:
2377:
2350:
2116:
5226:
2867:
3465:
3136:
3116:
3093:
2200:
2136:
2092:
2068:
5104:
64:
is a very similar algorithm. Although developed independently, it may also be seen as the instantiation of Knuth–Bendix algorithm in the theory of
5167:
5348:
5007:
4946:
4906:
5446:
3160:
3006:
5363:
5456:
5233:
5191:
790:
4547:
The order of the generators may crucially affect whether the Knuth–Bendix completion terminates. As an example, consider the
818:
1386:. Critical pair computation is an instance of paramodulation for equational unit clauses. "rw" is rewriting, implementing
5405:
5374:
1864:
285:
2382:
Next, we add more reductions (that is, rewriting rules) to eliminate possible exceptions of confluence. Suppose that
1852:
40:
825:(>) on the set of all terms; it is lifted to a well-founded ordering (▻) on the set of rewrite rules by defining
5461:
5160:
1824:
1812:
47:
5205:
2071:
1872:
1836:
57:
5353:
4789:
4731:
4473:
4403:
4212:
4035:
1877:
1832:
1378:. The 10 starred equations turn out to constitute the resulting convergent rewrite system. "pm" is short for "
4885:
3251:. This is an infinite monoid but nevertheless, the Knuth–Bendix algorithm is able to solve the word problem.
2021:
5369:
5198:
3856:
3690:
2245:
2016:
773:(>) on the set of all terms, and attempts to construct a confluent and terminating term rewriting system
3364:
5338:
5263:
5219:
3138:
that might have reducible left sides (after checking if such rules have critical pairs with other rules).
2095:
872:
853:
5451:
5415:
5153:
5060:
4352:
4301:
3313:
3262:
1856:
1337:
43:
1961:
then the word problem is easily solved. A confluent rewriting system allows one to do precisely this.
4865:
5307:
5212:
5126:
4155:
3978:
3470:
2966:
281:
2205:
1848:
371:
148:
5395:
4844:
it does not finish for there are no finite convergent systems compatible with this latter order.
4548:
3806:
3640:
2926:
2288:
2145:
1379:
822:
770:
3752:
3527:
4104:
3927:
2770:
2731:
5123:
5003:
4942:
4902:
4718:{\displaystyle \langle x,y,x^{-1},y^{-1}\,|\,xy=yx,xx^{-1}=x^{-1}x=yy^{-1}=y^{-1}y=1\rangle .}
2605:
2569:
2533:
2497:
1860:
245:
2809:
2698:
5089:
5035:
4934:
4854:
1355:
61:
5024:
3613:
3575:
3423:
2899:
2872:
2671:
2644:
2470:
2443:
2412:
2385:
2355:
2328:
5410:
5292:
5111:
256–276, London Math. Soc. Lecture Note Ser., 304, Cambridge Univ. Press, Cambridge, 2003.
4979:
2101:
886:
128:
109:
65:
21:
2846:
4963:
Bachmair, L.; Dershowitz, N.; Hsiang, J. (Jun 1986). "Orderings for
Equational Proofs".
5297:
5074:
5039:
4923:
4858:
3450:
3248:
3121:
3101:
3078:
2185:
2139:
2121:
2077:
2053:
1827:
are string rewriting systems which can be used to give canonical labels to elements or
4786:
finishes with a convergent system, however considering the length-lexicographic order
5440:
5390:
5093:
25:
4986:. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.
5176:
1966:
814:
766:
36:
5000:
Combinatorial and
Geometric Group Theory: Dortmund and Ottawa-Montreal conferences
3003:, then we have an instance where confluence could fail. Hence, add the reduction
5140:
5400:
2098:
giving the rewriting system. Suppose further that we have a reduction ordering
817:, the following inference rules can be used to transform it into an equivalent
100:) is the set of all equations that can be derived by applying equations from
4897:
Jacob T. Schwartz; Domenico
Cantone; Eugenio G. Omodeo; Martin Davis (2011).
5425:
5330:
5287:
5131:
4938:
1982:. An order that is both translation-invariant and a well-order is called a
28:
206:) is the set of all equations that can be confirmed by applying rules from
5075:"A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm"
5257:
5244:
4899:
Computational Logic and Set Theory: Applying
Formalized Logic to Analysis
3141:
Repeat the procedure until all overlapping left sides have been checked.
32:
5100:
C. Sims. 'Computations with finitely presented groups.' Cambridge, 1994.
5420:
793:, which gives an example proof from group theory, performed both using
51:
210:
left-to-right to both sides until they are literally equal. Formally,
1947:
in the class. If there is a computable method to determine for each
1998:
it is possible to end up with two different irreducible reductions W
1828:
5320:
5279:
5268:
4933:. Lecture Notes in Computer Science. Vol. 267. p. 54.
4728:
The Knuth–Bendix completion with respect to lexicographic order
730:
similar to above, since a right-to-left application of the rule
5149:
5145:
5315:
5252:
5023:
Bachmair, Leo; Dershowitz, Nachum; Plaisted, David A. (1989).
3236:{\displaystyle \langle x,y\mid x^{3}=y^{3}=(xy)^{3}=1\rangle }
1398:. Orienting of equations is done implicitly and not recorded.
3068:{\displaystyle \max r_{1},r_{2}\rightarrow \min r_{1},r_{2}}
2011:
Description of the algorithm for finitely presented monoids
785:
often requires human intuition, proving consequences from
46:. When the algorithm succeeds, it effectively solves the
683:
s deductive closure. However, there is no way to derive
1863:
which states that if an (abstract) rewriting system is
4901:. Springer Science & Business Media. p. 200.
5002:. Springer Science & Business Media. p. 62.
4792:
4734:
4560:
4476:
4406:
4355:
4304:
4215:
4158:
4107:
4038:
3981:
3930:
3859:
3809:
3755:
3693:
3643:
3616:
3578:
3530:
3473:
3453:
3426:
3367:
3316:
3265:
3163:
3124:
3104:
3081:
3009:
2969:
2929:
2902:
2875:
2849:
2812:
2773:
2734:
2701:
2674:
2647:
2608:
2572:
2536:
2500:
2473:
2446:
2415:
2388:
2358:
2331:
2291:
2248:
2208:
2188:
2148:
2124:
2104:
2080:
2056:
2024:
1880:
1925:
it is desirable to choose a standard representative
5383:
5329:
5306:
5278:
5243:
5183:
2494:, or vice versa. In the former case, we can write
1839:. This special case is the focus of this section.
791:
Confluence (abstract rewriting)#Motivating examples
4836:
4778:
4717:
4514:
4444:
4374:
4323:
4253:
4196:
4132:
4076:
4019:
3955:
3890:
3840:
3783:
3724:
3674:
3629:
3596:
3558:
3516:
3459:
3439:
3395:
3335:
3284:
3235:
3130:
3110:
3087:
3067:
2995:
2955:
2915:
2888:
2861:
2831:
2798:
2759:
2720:
2695:, or vice versa. In the former case, we can write
2687:
2660:
2630:
2594:
2558:
2522:
2486:
2459:
2428:
2401:
2371:
2344:
2317:
2274:
2234:
2194:
2174:
2130:
2110:
2086:
2062:
2042:
1904:
605: and
4965:Proc. IEEE Symposium on Logic in Computer Science
3039:
3010:
5227:Things a Computer Scientist Rarely Talks About
5105:Logged rewriting and identities among relators
821:(if possible): They are based on a user-given
5161:
4886:D. Knuth, "The Genesis of Attribute Grammars"
3254:Our beginning three reductions are therefore
1974:A < B → XAY < XBY for all words A,B,X,Y
1855:(or weakly confluent) if and only if all its
1354:The following example run, obtained from the
8:
5059:D. Knuth; P. Bendix (1970). J. Leech (ed.).
4709:
4561:
3230:
3164:
2668:is completely contained in (surrounded by)
2242:. Thus we begin with the set of reductions
2037:
2025:
1899:
1887:
4293:Now, we are left with the rewriting system
5168:
5154:
5146:
5109:Groups St. Andrews 2001 in Oxford. Vol. I,
5062:Simple Word Problems in Universal Algebras
4837:{\displaystyle x<y<x^{-1}<y^{-1}}
4779:{\displaystyle x<x^{-1}<y<y^{-1}}
4515:{\displaystyle y^{2}x^{2}\rightarrow xyxy}
4445:{\displaystyle yxyx\rightarrow x^{2}y^{2}}
4254:{\displaystyle y^{2}x^{2}\rightarrow xyxy}
4077:{\displaystyle yxyx\rightarrow x^{2}y^{2}}
1815:for another presentation of this example.
1482:initial("GROUP.lop", at_line_15_column_1)
1463:initial("GROUP.lop", at_line_12_column_1)
4924:"On word problems in equational theories"
4825:
4809:
4791:
4767:
4745:
4733:
4691:
4675:
4653:
4637:
4611:
4606:
4605:
4596:
4580:
4559:
4491:
4481:
4475:
4436:
4426:
4405:
4360:
4354:
4309:
4303:
4230:
4220:
4214:
4188:
4178:
4157:
4124:
4106:
4068:
4058:
4037:
4011:
4001:
3980:
3935:
3929:
3882:
3858:
3832:
3808:
3775:
3754:
3716:
3692:
3666:
3642:
3621:
3615:
3577:
3535:
3529:
3487:
3472:
3452:
3431:
3425:
3381:
3366:
3321:
3315:
3270:
3264:
3218:
3196:
3183:
3162:
3123:
3103:
3080:
3059:
3046:
3030:
3017:
3008:
2987:
2974:
2968:
2947:
2934:
2928:
2907:
2901:
2880:
2874:
2848:
2817:
2811:
2778:
2772:
2739:
2733:
2706:
2700:
2679:
2673:
2652:
2646:
2613:
2607:
2577:
2571:
2541:
2535:
2505:
2499:
2478:
2472:
2451:
2445:
2420:
2414:
2393:
2387:
2363:
2357:
2336:
2330:
2309:
2296:
2290:
2266:
2253:
2247:
2226:
2213:
2207:
2187:
2166:
2153:
2147:
2123:
2103:
2079:
2055:
2023:
1905:{\displaystyle M=\langle X\mid R\rangle }
1879:
1444:initial("GROUP.lop", at_line_9_column_1)
5426:Potrzebie system of weights and measures
1819:String rewriting systems in group theory
1400:
5359:Robinson–Schensted–Knuth correspondence
4878:
2043:{\displaystyle \langle X\mid R\rangle }
1851:states that a term rewriting system is
777:that has the same deductive closure as
761:The Knuth–Bendix algorithm takes a set
214:is again viewed as a binary relation, (
3891:{\displaystyle xyxyx\rightarrow y^{2}}
3725:{\displaystyle yxyxy\rightarrow x^{2}}
2275:{\displaystyle P_{i}\rightarrow Q_{i}}
3396:{\displaystyle (xy)^{3}\rightarrow 1}
1932:. This representative is called the
1859:are convergent. Furthermore, we have
999:} ›
975:} ›
7:
4922:Hsiang, J.; Rusinowitch, M. (1987).
4467:
4397:
4346:
4295:
4206:
4029:
3850:
3684:
3358:
3307:
3256:
5127:"Knuth–Bendix Completion Algorithm"
5068:. Pergamon Press. pp. 263–297.
4931:Automata, Languages and Programming
5141:Knuth-Bendix Completion Visualizer
5040:10.1016/B978-0-12-046371-8.50007-9
4375:{\displaystyle y^{3}\rightarrow 1}
4324:{\displaystyle x^{3}\rightarrow 1}
3336:{\displaystyle y^{3}\rightarrow 1}
3285:{\displaystyle x^{3}\rightarrow 1}
781:. While proving consequences from
14:
5344:Knuth–Bendix completion algorithm
5103:Anne Heyworth and C.D. Wensley. "
18:Knuth–Bendix completion algorithm
789:does not. For more details, see
5192:The Art of Computer Programming
4982:(1990). Jan van Leeuwen (ed.).
4197:{\displaystyle xyxy=y^{2}x^{2}}
4020:{\displaystyle yxyx=x^{2}y^{2}}
3517:{\displaystyle (xy)^{3}=xyxyxy}
2996:{\displaystyle r_{1}\neq r_{2}}
978:⊢
544:is a "rewrite rule" version of
4607:
4497:
4419:
4366:
4315:
4236:
4051:
3915:Both of these rules obsolete (
3875:
3709:
3484:
3474:
3387:
3378:
3368:
3327:
3276:
3215:
3205:
3036:
2259:
2235:{\displaystyle Q_{i}<P_{i}}
819:convergent term rewrite system
1:
2440:Case 1: either the prefix of
2118:among the words generated by
374:axioms, the derivation chain
286:reflexive transitive closures
5349:Knuth–Morris–Pratt algorithm
5094:10.1016/0022-0000(81)90002-7
5025:"Completion Without Failure"
4551:by the monoid presentation:
3682:, giving the reduction rule
954:
5364:Trabb Pardo–Knuth algorithm
4529:
4458:
4388:
4337:
4286:
4280:
4148:
4142:
3971:
3965:
3917:
3841:{\displaystyle xyxyx=y^{2}}
3799:
3793:
3675:{\displaystyle yxyxy=x^{2}}
3606:
3568:
2956:{\displaystyle r_{1},r_{2}}
2318:{\displaystyle P_{i}=Q_{i}}
2175:{\displaystyle P_{i}=Q_{i}}
1795:
1776:
1757:
1738:
1719:
1700:
1681:
1662:
1643:
1624:
1605:
1586:
1567:
1548:
1529:
1510:
1491:
1472:
1453:
1434:
1410:
229:) is its rewrite closure, (
5478:
5447:Computational group theory
3784:{\displaystyle xyxyxy^{3}}
3559:{\displaystyle x^{3}yxyxy}
1843:Motivation in group theory
1825:computational group theory
1813:Word problem (mathematics)
31:for transforming a set of
5406:Knuth's up-arrow notation
5375:Knuth's Simpath algorithm
5206:Computers and Typesetting
4853:equations and produces a
4543:A non-terminating example
4133:{\displaystyle xyxyx^{3}}
3956:{\displaystyle x^{3}yxyx}
2923:first. Call the results
2799:{\displaystyle P_{i}=ABC}
2760:{\displaystyle P_{j}=ABC}
1873:finitely presented monoid
2631:{\displaystyle P_{j}=BC}
2595:{\displaystyle P_{i}=AB}
2559:{\displaystyle P_{j}=AB}
2523:{\displaystyle P_{i}=BC}
2325:can be reduced, replace
1978:This property is called
1833:finitely presented group
548:, the derivation chains
497:s deductive closure. If
104:in any order. Formally,
5199:The Complexity of Songs
4939:10.1007/3-540-18088-5_6
3848:. Hence the reduction
3524:, so consider the word
3098:After adding a rule to
2832:{\displaystyle P_{j}=B}
2721:{\displaystyle P_{i}=B}
2285:First, if any relation
2015:Suppose we are given a
24:and Peter Bendix) is a
5457:Combinatorics on words
5234:Selected papers series
4861:for the word problem.
4838:
4780:
4719:
4516:
4446:
4376:
4325:
4290:), so we remove them.
4278:These obsolete rules (
4255:
4198:
4134:
4078:
4021:
3957:
3892:
3842:
3785:
3726:
3676:
3631:
3598:
3560:
3518:
3461:
3441:
3397:
3337:
3286:
3237:
3154:Consider the monoid:
3132:
3118:, remove any rules in
3112:
3089:
3069:
2997:
2957:
2917:
2890:
2863:
2833:
2800:
2767:; in the latter case,
2761:
2722:
2689:
2662:
2632:
2596:
2566:; in the latter case,
2560:
2524:
2488:
2461:
2430:
2403:
2373:
2346:
2319:
2276:
2236:
2196:
2176:
2142:). For each relation
2132:
2112:
2088:
2064:
2044:
1980:translation invariance
1906:
873:encompassment ordering
170:of rewrite rules, its
58:Buchberger's algorithm
5416:Quater-imaginary base
4988:Here: sect.8.1, p.293
4839:
4781:
4720:
4517:
4447:
4377:
4326:
4256:
4204:, so we add the rule
4199:
4135:
4079:
4027:, so we add the rule
4022:
3958:
3893:
3843:
3786:
3727:
3677:
3632:
3630:{\displaystyle x^{2}}
3599:
3597:{\displaystyle yxyxy}
3561:
3519:
3462:
3442:
3440:{\displaystyle x^{3}}
3398:
3338:
3287:
3238:
3150:A terminating example
3133:
3113:
3090:
3070:
2998:
2958:
2918:
2916:{\displaystyle P_{j}}
2891:
2889:{\displaystyle P_{i}}
2864:
2834:
2801:
2762:
2723:
2690:
2688:{\displaystyle P_{j}}
2663:
2661:{\displaystyle P_{i}}
2633:
2597:
2561:
2525:
2489:
2487:{\displaystyle P_{j}}
2467:equals the suffix of
2462:
2460:{\displaystyle P_{i}}
2431:
2429:{\displaystyle P_{j}}
2404:
2402:{\displaystyle P_{i}}
2379:with the reductions.
2374:
2372:{\displaystyle Q_{i}}
2347:
2345:{\displaystyle P_{i}}
2320:
2277:
2237:
2197:
2177:
2133:
2113:
2089:
2065:
2045:
1907:
1823:An important case in
813:of equations between
765:of equations between
44:term rewriting system
5370:Dijkstra's algorithm
5308:Literate programming
5213:Concrete Mathematics
5082:J. Comput. Syst. Sci
5073:Gérard Huet (1981).
5032:Rewriting Techniques
4857:system, providing a
4790:
4732:
4558:
4474:
4404:
4353:
4302:
4213:
4156:
4105:
4036:
3979:
3928:
3921:), so we remove it.
3857:
3807:
3791:and reducing using (
3753:
3691:
3641:
3614:
3576:
3528:
3471:
3451:
3424:
3365:
3314:
3263:
3161:
3122:
3102:
3079:
3007:
2967:
2963:, respectively. If
2927:
2900:
2873:
2847:
2810:
2771:
2732:
2699:
2672:
2645:
2606:
2570:
2534:
2498:
2471:
2444:
2413:
2386:
2356:
2329:
2289:
2246:
2206:
2186:
2146:
2122:
2111:{\displaystyle <}
2102:
2078:
2054:
2022:
1878:
1865:strongly normalizing
282:relation composition
5339:Knuth's Algorithm X
4967:. pp. 346–357.
3975:). Reducing we get
3604:. Reducing using (
3566:. Reducing using (
2862:{\displaystyle ABC}
1849:critical pair lemma
1835:as products of the
1511:f(X,f(Y,i(f(X,Y))))
149:equivalence closure
5396:Knuth reward check
5368:Generalization of
5124:Weisstein, Eric W.
4834:
4776:
4715:
4549:free Abelian group
4512:
4442:
4372:
4321:
4251:
4194:
4130:
4074:
4017:
3953:
3888:
3838:
3781:
3722:
3672:
3627:
3594:
3556:
3514:
3457:
3437:
3393:
3333:
3282:
3233:
3128:
3108:
3085:
3065:
2993:
2953:
2913:
2896:first, then using
2886:
2859:
2829:
2796:
2757:
2718:
2685:
2658:
2628:
2592:
2556:
2520:
2484:
2457:
2426:
2399:
2369:
2342:
2315:
2272:
2232:
2192:
2172:
2128:
2108:
2084:
2060:
2040:
1902:
823:reduction ordering
771:reduction ordering
633:demonstrate that (
462:demonstrates that
80:of equations, its
50:for the specified
5462:Rewriting systems
5434:
5433:
5009:978-3-7643-9911-5
4948:978-3-540-18088-3
4908:978-0-85729-808-9
4537:
4536:
4466:
4465:
4396:
4395:
4345:
4344:
4276:
4275:
4099:
4098:
3913:
3912:
3749:Similarly, using
3747:
3746:
3637:. Hence, we get
3467:) is a prefix of
3460:{\displaystyle x}
3418:
3417:
3357:
3356:
3306:
3305:
3131:{\displaystyle R}
3111:{\displaystyle R}
3088:{\displaystyle R}
2195:{\displaystyle R}
2131:{\displaystyle X}
2087:{\displaystyle R}
2063:{\displaystyle X}
1853:locally confluent
1809:
1808:
1347:
1346:
887:literally similar
172:deductive closure
82:deductive closure
5469:
5170:
5163:
5156:
5147:
5137:
5136:
5097:
5079:
5069:
5067:
5051:
5050:
5048:
5046:
5029:
5020:
5014:
5013:
4995:
4989:
4987:
4975:
4969:
4968:
4960:
4954:
4952:
4928:
4919:
4913:
4912:
4894:
4888:
4883:
4866:logged rewriting
4855:ground confluent
4843:
4841:
4840:
4835:
4833:
4832:
4817:
4816:
4785:
4783:
4782:
4777:
4775:
4774:
4753:
4752:
4724:
4722:
4721:
4716:
4699:
4698:
4683:
4682:
4661:
4660:
4645:
4644:
4610:
4604:
4603:
4588:
4587:
4521:
4519:
4518:
4513:
4496:
4495:
4486:
4485:
4468:
4451:
4449:
4448:
4443:
4441:
4440:
4431:
4430:
4398:
4381:
4379:
4378:
4373:
4365:
4364:
4347:
4330:
4328:
4327:
4322:
4314:
4313:
4296:
4270:
4260:
4258:
4257:
4252:
4235:
4234:
4225:
4224:
4207:
4203:
4201:
4200:
4195:
4193:
4192:
4183:
4182:
4140:by overlapping (
4139:
4137:
4136:
4131:
4129:
4128:
4093:
4083:
4081:
4080:
4075:
4073:
4072:
4063:
4062:
4030:
4026:
4024:
4023:
4018:
4016:
4015:
4006:
4005:
3963:by overlapping (
3962:
3960:
3959:
3954:
3940:
3939:
3907:
3897:
3895:
3894:
3889:
3887:
3886:
3851:
3847:
3845:
3844:
3839:
3837:
3836:
3790:
3788:
3787:
3782:
3780:
3779:
3741:
3731:
3729:
3728:
3723:
3721:
3720:
3685:
3681:
3679:
3678:
3673:
3671:
3670:
3636:
3634:
3633:
3628:
3626:
3625:
3603:
3601:
3600:
3595:
3565:
3563:
3562:
3557:
3540:
3539:
3523:
3521:
3520:
3515:
3492:
3491:
3466:
3464:
3463:
3458:
3446:
3444:
3443:
3438:
3436:
3435:
3412:
3402:
3400:
3399:
3394:
3386:
3385:
3359:
3351:
3342:
3340:
3339:
3334:
3326:
3325:
3308:
3300:
3291:
3289:
3288:
3283:
3275:
3274:
3257:
3242:
3240:
3239:
3234:
3223:
3222:
3201:
3200:
3188:
3187:
3137:
3135:
3134:
3129:
3117:
3115:
3114:
3109:
3094:
3092:
3091:
3086:
3074:
3072:
3071:
3066:
3064:
3063:
3051:
3050:
3035:
3034:
3022:
3021:
3002:
3000:
2999:
2994:
2992:
2991:
2979:
2978:
2962:
2960:
2959:
2954:
2952:
2951:
2939:
2938:
2922:
2920:
2919:
2914:
2912:
2911:
2895:
2893:
2892:
2887:
2885:
2884:
2868:
2866:
2865:
2860:
2843:Reduce the word
2838:
2836:
2835:
2830:
2822:
2821:
2805:
2803:
2802:
2797:
2783:
2782:
2766:
2764:
2763:
2758:
2744:
2743:
2727:
2725:
2724:
2719:
2711:
2710:
2694:
2692:
2691:
2686:
2684:
2683:
2667:
2665:
2664:
2659:
2657:
2656:
2637:
2635:
2634:
2629:
2618:
2617:
2601:
2599:
2598:
2593:
2582:
2581:
2565:
2563:
2562:
2557:
2546:
2545:
2529:
2527:
2526:
2521:
2510:
2509:
2493:
2491:
2490:
2485:
2483:
2482:
2466:
2464:
2463:
2458:
2456:
2455:
2435:
2433:
2432:
2427:
2425:
2424:
2408:
2406:
2405:
2400:
2398:
2397:
2378:
2376:
2375:
2370:
2368:
2367:
2351:
2349:
2348:
2343:
2341:
2340:
2324:
2322:
2321:
2316:
2314:
2313:
2301:
2300:
2281:
2279:
2278:
2273:
2271:
2270:
2258:
2257:
2241:
2239:
2238:
2233:
2231:
2230:
2218:
2217:
2201:
2199:
2198:
2193:
2181:
2179:
2178:
2173:
2171:
2170:
2158:
2157:
2137:
2135:
2134:
2129:
2117:
2115:
2114:
2109:
2093:
2091:
2090:
2085:
2069:
2067:
2066:
2061:
2049:
2047:
2046:
2041:
1954:its normal form
1911:
1909:
1908:
1903:
1401:
1382:", implementing
1373:
1361:
1356:E theorem prover
1335:
1276:
1256:
1246:
1242:
1241:
1240:
1239:
1233:
1168:
1103:
1099:
1098:
1097:
1096:
1090:
1024:
1020:
1019:
1018:
1017:
1011:
903:
902:
898:
884:
880:
870:
865:
864:
863:
862:
858:
844:
758:is not allowed.
757:
726:
725:
724:
719:
716:
710:
709:
708:
703:
700:
675:
674:
673:
668:
665:
659:
658:
657:
652:
649:
629:
624:
623:
622:
617:
614:
600:
599:
598:
593:
590:
580:
579:
578:
573:
570:
543:
489:
488:
487:
482:
479:
458:
453:
452:
451:
446:
443:
433:
432:
431:
426:
423:
405:
404:
403:
398:
395:
369:
323:For example, if
319:
318:
317:
312:
309:
303:
302:
301:
296:
293:
279:
278:
277:
272:
269:
263:
262:
261:
256:
253:
243:
242:
241:
240:
234:
228:
227:
226:
225:
219:
205:
204:
203:
198:
195:
189:
188:
187:
182:
179:
165:
164:
163:
162:
156:
146:
145:
144:
139:
136:
126:
125:
124:
123:
117:
108:is considered a
99:
98:
97:
92:
89:
66:polynomial rings
5477:
5476:
5472:
5471:
5470:
5468:
5467:
5466:
5437:
5436:
5435:
5430:
5411:Man or boy test
5379:
5325:
5302:
5293:Computer Modern
5274:
5239:
5220:Surreal Numbers
5179:
5174:
5122:
5121:
5118:
5077:
5072:
5065:
5058:
5055:
5054:
5044:
5042:
5027:
5022:
5021:
5017:
5010:
4997:
4996:
4992:
4984:Rewrite Systems
4980:J.-P. Jouannaud
4978:N. Dershowitz;
4977:
4976:
4972:
4962:
4961:
4957:
4949:
4926:
4921:
4920:
4916:
4909:
4896:
4895:
4891:
4884:
4880:
4875:
4850:
4848:Generalizations
4821:
4805:
4788:
4787:
4763:
4741:
4730:
4729:
4687:
4671:
4649:
4633:
4592:
4576:
4556:
4555:
4545:
4487:
4477:
4472:
4471:
4432:
4422:
4402:
4401:
4356:
4351:
4350:
4305:
4300:
4299:
4268:
4226:
4216:
4211:
4210:
4184:
4174:
4154:
4153:
4120:
4103:
4102:
4091:
4064:
4054:
4034:
4033:
4007:
3997:
3977:
3976:
3931:
3926:
3925:
3924:Next, consider
3905:
3878:
3855:
3854:
3828:
3805:
3804:
3771:
3751:
3750:
3739:
3712:
3689:
3688:
3662:
3639:
3638:
3617:
3612:
3611:
3574:
3573:
3531:
3526:
3525:
3483:
3469:
3468:
3449:
3448:
3427:
3422:
3421:
3410:
3377:
3363:
3362:
3349:
3317:
3312:
3311:
3298:
3266:
3261:
3260:
3214:
3192:
3179:
3159:
3158:
3152:
3147:
3120:
3119:
3100:
3099:
3077:
3076:
3055:
3042:
3026:
3013:
3005:
3004:
2983:
2970:
2965:
2964:
2943:
2930:
2925:
2924:
2903:
2898:
2897:
2876:
2871:
2870:
2845:
2844:
2813:
2808:
2807:
2774:
2769:
2768:
2735:
2730:
2729:
2702:
2697:
2696:
2675:
2670:
2669:
2648:
2643:
2642:
2641:Case 2: either
2609:
2604:
2603:
2573:
2568:
2567:
2537:
2532:
2531:
2501:
2496:
2495:
2474:
2469:
2468:
2447:
2442:
2441:
2416:
2411:
2410:
2389:
2384:
2383:
2359:
2354:
2353:
2332:
2327:
2326:
2305:
2292:
2287:
2286:
2262:
2249:
2244:
2243:
2222:
2209:
2204:
2203:
2184:
2183:
2162:
2149:
2144:
2143:
2120:
2119:
2100:
2099:
2076:
2075:
2052:
2051:
2020:
2019:
2013:
2005:
2002: ≠ W'
2001:
1997:
1993:
1984:reduction order
1959:
1952:
1945:
1930:
1922:
1918:
1876:
1875:
1845:
1821:
1371:
1359:
1352:
1325:
1258:
1248:
1235:
1234:
1231:
1230:
1229:
1225:
1160:
1092:
1091:
1088:
1087:
1086:
1082:
1013:
1012:
1009:
1008:
1007:
1003:
890:
882:
878:
860:
859:
856:
855:
854:
849:
826:
807:
731:
720:
717:
714:
713:
712:
704:
701:
698:
697:
696:
679:is a member of
669:
666:
663:
662:
661:
653:
650:
647:
646:
645:
618:
615:
612:
611:
610:
594:
591:
588:
587:
586:
574:
571:
568:
567:
566:
552:
498:
493:is a member of
483:
480:
477:
476:
475:
447:
444:
441:
440:
439:
427:
424:
421:
420:
419:
399:
396:
393:
392:
391:
378:
324:
313:
310:
307:
306:
305:
297:
294:
291:
290:
289:
273:
270:
267:
266:
265:
257:
254:
251:
250:
249:
236:
235:
232:
231:
230:
221:
220:
217:
216:
215:
199:
196:
193:
192:
191:
183:
180:
177:
176:
175:
158:
157:
154:
153:
152:
140:
137:
134:
133:
132:
129:rewrite closure
119:
118:
115:
114:
113:
110:binary relation
93:
90:
87:
86:
85:
74:
12:
11:
5:
5475:
5473:
5465:
5464:
5459:
5454:
5449:
5439:
5438:
5432:
5431:
5429:
5428:
5423:
5418:
5413:
5408:
5403:
5398:
5393:
5387:
5385:
5381:
5380:
5378:
5377:
5372:
5366:
5361:
5356:
5351:
5346:
5341:
5335:
5333:
5327:
5326:
5324:
5323:
5318:
5312:
5310:
5304:
5303:
5301:
5300:
5298:Concrete Roman
5295:
5290:
5284:
5282:
5276:
5275:
5273:
5272:
5266:
5260:
5255:
5249:
5247:
5241:
5240:
5238:
5237:
5230:
5223:
5216:
5209:
5202:
5195:
5187:
5185:
5181:
5180:
5175:
5173:
5172:
5165:
5158:
5150:
5144:
5143:
5138:
5117:
5116:External links
5114:
5113:
5112:
5101:
5098:
5070:
5053:
5052:
5015:
5008:
4990:
4970:
4955:
4947:
4914:
4907:
4889:
4877:
4876:
4874:
4871:
4864:The notion of
4859:semi-algorithm
4849:
4846:
4831:
4828:
4824:
4820:
4815:
4812:
4808:
4804:
4801:
4798:
4795:
4773:
4770:
4766:
4762:
4759:
4756:
4751:
4748:
4744:
4740:
4737:
4726:
4725:
4714:
4711:
4708:
4705:
4702:
4697:
4694:
4690:
4686:
4681:
4678:
4674:
4670:
4667:
4664:
4659:
4656:
4652:
4648:
4643:
4640:
4636:
4632:
4629:
4626:
4623:
4620:
4617:
4614:
4609:
4602:
4599:
4595:
4591:
4586:
4583:
4579:
4575:
4572:
4569:
4566:
4563:
4544:
4541:
4535:
4534:
4525:
4523:
4511:
4508:
4505:
4502:
4499:
4494:
4490:
4484:
4480:
4464:
4463:
4454:
4452:
4439:
4435:
4429:
4425:
4421:
4418:
4415:
4412:
4409:
4394:
4393:
4384:
4382:
4371:
4368:
4363:
4359:
4343:
4342:
4333:
4331:
4320:
4317:
4312:
4308:
4274:
4273:
4264:
4262:
4250:
4247:
4244:
4241:
4238:
4233:
4229:
4223:
4219:
4191:
4187:
4181:
4177:
4173:
4170:
4167:
4164:
4161:
4127:
4123:
4119:
4116:
4113:
4110:
4097:
4096:
4087:
4085:
4071:
4067:
4061:
4057:
4053:
4050:
4047:
4044:
4041:
4014:
4010:
4004:
4000:
3996:
3993:
3990:
3987:
3984:
3952:
3949:
3946:
3943:
3938:
3934:
3911:
3910:
3901:
3899:
3885:
3881:
3877:
3874:
3871:
3868:
3865:
3862:
3835:
3831:
3827:
3824:
3821:
3818:
3815:
3812:
3778:
3774:
3770:
3767:
3764:
3761:
3758:
3745:
3744:
3735:
3733:
3719:
3715:
3711:
3708:
3705:
3702:
3699:
3696:
3669:
3665:
3661:
3658:
3655:
3652:
3649:
3646:
3624:
3620:
3593:
3590:
3587:
3584:
3581:
3555:
3552:
3549:
3546:
3543:
3538:
3534:
3513:
3510:
3507:
3504:
3501:
3498:
3495:
3490:
3486:
3482:
3479:
3476:
3456:
3434:
3430:
3416:
3415:
3406:
3404:
3392:
3389:
3384:
3380:
3376:
3373:
3370:
3355:
3354:
3345:
3343:
3332:
3329:
3324:
3320:
3304:
3303:
3294:
3292:
3281:
3278:
3273:
3269:
3249:shortlex order
3245:
3244:
3232:
3229:
3226:
3221:
3217:
3213:
3210:
3207:
3204:
3199:
3195:
3191:
3186:
3182:
3178:
3175:
3172:
3169:
3166:
3151:
3148:
3146:
3143:
3127:
3107:
3084:
3062:
3058:
3054:
3049:
3045:
3041:
3038:
3033:
3029:
3025:
3020:
3016:
3012:
2990:
2986:
2982:
2977:
2973:
2950:
2946:
2942:
2937:
2933:
2910:
2906:
2883:
2879:
2858:
2855:
2852:
2841:
2840:
2828:
2825:
2820:
2816:
2795:
2792:
2789:
2786:
2781:
2777:
2756:
2753:
2750:
2747:
2742:
2738:
2717:
2714:
2709:
2705:
2682:
2678:
2655:
2651:
2639:
2627:
2624:
2621:
2616:
2612:
2591:
2588:
2585:
2580:
2576:
2555:
2552:
2549:
2544:
2540:
2519:
2516:
2513:
2508:
2504:
2481:
2477:
2454:
2450:
2423:
2419:
2396:
2392:
2366:
2362:
2339:
2335:
2312:
2308:
2304:
2299:
2295:
2269:
2265:
2261:
2256:
2252:
2229:
2225:
2221:
2216:
2212:
2191:
2169:
2165:
2161:
2156:
2152:
2140:shortlex order
2127:
2107:
2083:
2059:
2039:
2036:
2033:
2030:
2027:
2012:
2009:
2003:
1999:
1995:
1994: → W
1991:
1976:
1975:
1957:
1950:
1943:
1940:for each word
1928:
1920:
1916:
1901:
1898:
1895:
1892:
1889:
1886:
1883:
1861:Newman's lemma
1857:critical pairs
1844:
1841:
1820:
1817:
1807:
1806:
1803:
1800:
1797:
1794:
1792:
1788:
1787:
1784:
1783:f(Y,i(f(X,Y)))
1781:
1778:
1775:
1773:
1769:
1768:
1765:
1764:f(Y,i(f(X,Y)))
1762:
1759:
1756:
1754:
1750:
1749:
1746:
1745:f(i(X),f(X,Y))
1743:
1740:
1737:
1735:
1731:
1730:
1727:
1726:f(i(X),f(X,Y))
1724:
1721:
1718:
1716:
1712:
1711:
1708:
1705:
1702:
1699:
1697:
1693:
1692:
1689:
1686:
1683:
1680:
1678:
1674:
1673:
1670:
1667:
1664:
1663:f(X,f(i(X),Y))
1661:
1659:
1655:
1654:
1651:
1648:
1645:
1642:
1640:
1636:
1635:
1632:
1629:
1626:
1623:
1621:
1617:
1616:
1613:
1610:
1607:
1604:
1602:
1598:
1597:
1594:
1591:
1588:
1585:
1583:
1579:
1578:
1575:
1572:
1569:
1566:
1564:
1560:
1559:
1556:
1553:
1550:
1547:
1545:
1541:
1540:
1537:
1536:f(X,f(i(X),Y))
1534:
1531:
1528:
1526:
1522:
1521:
1518:
1515:
1512:
1509:
1507:
1503:
1502:
1499:
1496:
1493:
1490:
1488:
1484:
1483:
1480:
1477:
1474:
1471:
1469:
1465:
1464:
1461:
1458:
1455:
1452:
1450:
1446:
1445:
1442:
1439:
1436:
1433:
1431:
1427:
1426:
1421:
1416:
1414:
1409:
1407:
1380:paramodulation
1351:
1348:
1345:
1344:
1322:
1315:
1300:
1297:
1290:
1284:
1278:
1277:
1222:
1215:
1200:
1197:
1182:
1176:
1170:
1169:
1157:
1142:
1136:
1133:
1126:
1111:
1105:
1104:
1079:
1072:
1057:
1054:
1047:
1032:
1026:
1025:
1000:
985:
979:
976:
961:
955:
948:
947:
940:
934:
931:
924:
909:
901:
900:
876:
806:
803:
631:
630:
460:
459:
73:
70:
60:for computing
13:
10:
9:
6:
4:
3:
2:
5474:
5463:
5460:
5458:
5455:
5453:
5450:
5448:
5445:
5444:
5442:
5427:
5424:
5422:
5419:
5417:
5414:
5412:
5409:
5407:
5404:
5402:
5399:
5397:
5394:
5392:
5391:Dancing Links
5389:
5388:
5386:
5382:
5376:
5373:
5371:
5367:
5365:
5362:
5360:
5357:
5355:
5354:Knuth shuffle
5352:
5350:
5347:
5345:
5342:
5340:
5337:
5336:
5334:
5332:
5328:
5322:
5319:
5317:
5314:
5313:
5311:
5309:
5305:
5299:
5296:
5294:
5291:
5289:
5286:
5285:
5283:
5281:
5277:
5270:
5267:
5265:
5261:
5259:
5256:
5254:
5251:
5250:
5248:
5246:
5242:
5236:
5235:
5231:
5229:
5228:
5224:
5222:
5221:
5217:
5215:
5214:
5210:
5208:
5207:
5203:
5200:
5196:
5194:
5193:
5189:
5188:
5186:
5182:
5178:
5171:
5166:
5164:
5159:
5157:
5152:
5151:
5148:
5142:
5139:
5134:
5133:
5128:
5125:
5120:
5119:
5115:
5110:
5106:
5102:
5099:
5095:
5091:
5087:
5083:
5076:
5071:
5064:
5063:
5057:
5056:
5041:
5037:
5033:
5026:
5019:
5016:
5011:
5005:
5001:
4994:
4991:
4985:
4981:
4974:
4971:
4966:
4959:
4956:
4950:
4944:
4940:
4936:
4932:
4925:
4918:
4915:
4910:
4904:
4900:
4893:
4890:
4887:
4882:
4879:
4872:
4870:
4867:
4862:
4860:
4856:
4847:
4845:
4829:
4826:
4822:
4818:
4813:
4810:
4806:
4802:
4799:
4796:
4793:
4771:
4768:
4764:
4760:
4757:
4754:
4749:
4746:
4742:
4738:
4735:
4712:
4706:
4703:
4700:
4695:
4692:
4688:
4684:
4679:
4676:
4672:
4668:
4665:
4662:
4657:
4654:
4650:
4646:
4641:
4638:
4634:
4630:
4627:
4624:
4621:
4618:
4615:
4612:
4600:
4597:
4593:
4589:
4584:
4581:
4577:
4573:
4570:
4567:
4564:
4554:
4553:
4552:
4550:
4542:
4540:
4532:
4531:
4526:
4524:
4509:
4506:
4503:
4500:
4492:
4488:
4482:
4478:
4470:
4469:
4461:
4460:
4455:
4453:
4437:
4433:
4427:
4423:
4416:
4413:
4410:
4407:
4400:
4399:
4391:
4390:
4385:
4383:
4369:
4361:
4357:
4349:
4348:
4340:
4339:
4334:
4332:
4318:
4310:
4306:
4298:
4297:
4294:
4291:
4289:
4288:
4283:
4282:
4272:
4265:
4263:
4248:
4245:
4242:
4239:
4231:
4227:
4221:
4217:
4209:
4208:
4205:
4189:
4185:
4179:
4175:
4171:
4168:
4165:
4162:
4159:
4151:
4150:
4145:
4144:
4125:
4121:
4117:
4114:
4111:
4108:
4095:
4088:
4086:
4069:
4065:
4059:
4055:
4048:
4045:
4042:
4039:
4032:
4031:
4028:
4012:
4008:
4002:
3998:
3994:
3991:
3988:
3985:
3982:
3974:
3973:
3968:
3967:
3950:
3947:
3944:
3941:
3936:
3932:
3922:
3920:
3919:
3909:
3902:
3900:
3883:
3879:
3872:
3869:
3866:
3863:
3860:
3853:
3852:
3849:
3833:
3829:
3825:
3822:
3819:
3816:
3813:
3810:
3802:
3801:
3796:
3795:
3776:
3772:
3768:
3765:
3762:
3759:
3756:
3743:
3736:
3734:
3717:
3713:
3706:
3703:
3700:
3697:
3694:
3687:
3686:
3683:
3667:
3663:
3659:
3656:
3653:
3650:
3647:
3644:
3622:
3618:
3609:
3608:
3591:
3588:
3585:
3582:
3579:
3571:
3570:
3553:
3550:
3547:
3544:
3541:
3536:
3532:
3511:
3508:
3505:
3502:
3499:
3496:
3493:
3488:
3480:
3477:
3454:
3432:
3428:
3414:
3407:
3405:
3390:
3382:
3374:
3371:
3361:
3360:
3353:
3346:
3344:
3330:
3322:
3318:
3310:
3309:
3302:
3295:
3293:
3279:
3271:
3267:
3259:
3258:
3255:
3252:
3250:
3227:
3224:
3219:
3211:
3208:
3202:
3197:
3193:
3189:
3184:
3180:
3176:
3173:
3170:
3167:
3157:
3156:
3155:
3149:
3144:
3142:
3139:
3125:
3105:
3096:
3082:
3060:
3056:
3052:
3047:
3043:
3031:
3027:
3023:
3018:
3014:
2988:
2984:
2980:
2975:
2971:
2948:
2944:
2940:
2935:
2931:
2908:
2904:
2881:
2877:
2856:
2853:
2850:
2826:
2823:
2818:
2814:
2793:
2790:
2787:
2784:
2779:
2775:
2754:
2751:
2748:
2745:
2740:
2736:
2715:
2712:
2707:
2703:
2680:
2676:
2653:
2649:
2640:
2625:
2622:
2619:
2614:
2610:
2589:
2586:
2583:
2578:
2574:
2553:
2550:
2547:
2542:
2538:
2517:
2514:
2511:
2506:
2502:
2479:
2475:
2452:
2448:
2439:
2438:
2437:
2421:
2417:
2394:
2390:
2380:
2364:
2360:
2337:
2333:
2310:
2306:
2302:
2297:
2293:
2283:
2267:
2263:
2254:
2250:
2227:
2223:
2219:
2214:
2210:
2189:
2167:
2163:
2159:
2154:
2150:
2141:
2125:
2105:
2097:
2081:
2073:
2057:
2034:
2031:
2028:
2018:
2010:
2008:
1987:
1985:
1981:
1973:
1972:
1971:
1968:
1962:
1960:
1953:
1946:
1939:
1935:
1931:
1924:
1896:
1893:
1890:
1884:
1881:
1874:
1869:
1866:
1862:
1858:
1854:
1850:
1842:
1840:
1838:
1834:
1830:
1826:
1818:
1816:
1814:
1804:
1801:
1798:
1793:
1790:
1789:
1785:
1782:
1779:
1774:
1771:
1770:
1766:
1763:
1760:
1755:
1752:
1751:
1747:
1744:
1741:
1736:
1733:
1732:
1728:
1725:
1722:
1717:
1714:
1713:
1709:
1706:
1703:
1698:
1695:
1694:
1690:
1687:
1684:
1679:
1676:
1675:
1671:
1668:
1665:
1660:
1657:
1656:
1652:
1649:
1646:
1641:
1638:
1637:
1633:
1630:
1627:
1622:
1619:
1618:
1614:
1611:
1608:
1603:
1600:
1599:
1595:
1592:
1589:
1584:
1581:
1580:
1576:
1573:
1570:
1565:
1562:
1561:
1557:
1554:
1551:
1546:
1543:
1542:
1538:
1535:
1532:
1527:
1524:
1523:
1519:
1516:
1513:
1508:
1505:
1504:
1500:
1497:
1494:
1489:
1486:
1485:
1481:
1478:
1475:
1470:
1467:
1466:
1462:
1459:
1456:
1451:
1448:
1447:
1443:
1440:
1437:
1432:
1429:
1428:
1425:
1422:
1420:
1417:
1415:
1413:
1408:
1406:
1403:
1402:
1399:
1397:
1393:
1389:
1385:
1381:
1377:
1369:
1365:
1357:
1349:
1343:
1339:
1338:critical pair
1333:
1329:
1323:
1320:
1316:
1313:
1309:
1305:
1301:
1298:
1295:
1291:
1289:
1285:
1283:
1280:
1279:
1274:
1270:
1266:
1262:
1255:
1251:
1245:
1238:
1228:
1223:
1220:
1216:
1213:
1209:
1205:
1201:
1198:
1195:
1191:
1187:
1183:
1181:
1177:
1175:
1172:
1171:
1167:
1163:
1158:
1155:
1151:
1147:
1143:
1141:
1137:
1134:
1131:
1127:
1124:
1120:
1116:
1112:
1110:
1107:
1106:
1102:
1095:
1085:
1080:
1077:
1073:
1070:
1066:
1062:
1058:
1055:
1052:
1048:
1045:
1041:
1037:
1033:
1031:
1028:
1027:
1023:
1016:
1006:
1001:
998:
994:
990:
986:
984:
980:
977:
974:
970:
966:
962:
960:
956:
953:
950:
949:
945:
941:
939:
935:
932:
929:
925:
922:
918:
914:
910:
908:
905:
904:
897:
893:
888:
877:
874:
869:
866:
852:
848:
847:
846:
842:
838:
834:
830:
824:
820:
816:
812:
804:
802:
800:
796:
792:
788:
784:
780:
776:
772:
768:
764:
759:
755:
751:
747:
743:
739:
735:
729:
723:
707:
694:
690:
686:
682:
678:
672:
656:
644:
640:
636:
628:
621:
608:
604:
597:
584:
577:
564:
560:
556:
551:
550:
549:
547:
541:
537:
533:
529:
525:
521:
517:
513:
509:
505:
501:
496:
492:
486:
473:
469:
465:
457:
450:
437:
430:
417:
413:
409:
402:
389:
385:
381:
377:
376:
375:
373:
367:
363:
359:
355:
351:
347:
343:
339:
335:
331:
327:
321:
316:
300:
287:
283:
276:
260:
247:
239:
224:
213:
209:
202:
186:
173:
169:
166:). For a set
161:
150:
143:
130:
122:
111:
107:
103:
96:
83:
79:
71:
69:
67:
63:
62:Gröbner bases
59:
55:
53:
49:
45:
42:
38:
34:
30:
27:
26:semi-decision
23:
20:(named after
19:
5452:Donald Knuth
5343:
5232:
5225:
5218:
5211:
5204:
5190:
5184:Publications
5177:Donald Knuth
5130:
5108:
5088:(1): 11–21.
5085:
5081:
5061:
5043:. Retrieved
5031:
5018:
4999:
4993:
4983:
4973:
4964:
4958:
4930:
4917:
4898:
4892:
4881:
4863:
4851:
4727:
4546:
4538:
4528:
4457:
4387:
4336:
4292:
4285:
4279:
4277:
4266:
4147:
4141:
4101:Considering
4100:
4089:
3970:
3964:
3923:
3916:
3914:
3903:
3798:
3792:
3748:
3737:
3605:
3567:
3420:A suffix of
3419:
3408:
3347:
3296:
3253:
3246:
3153:
3140:
3097:
2842:
2381:
2284:
2094:is a set of
2070:is a set of
2017:presentation
2014:
1988:
1983:
1979:
1977:
1967:well-ordered
1963:
1955:
1948:
1941:
1937:
1933:
1926:
1914:
1870:
1846:
1822:
1810:
1796:f(i(X),i(Y))
1593:f(X,i(i(Y)))
1574:f(0,i(i(X)))
1555:f(0,i(i(X)))
1423:
1418:
1411:
1404:
1395:
1391:
1387:
1383:
1375:
1367:
1363:
1353:
1341:
1331:
1327:
1318:
1311:
1307:
1303:
1293:
1287:
1281:
1272:
1268:
1264:
1260:
1253:
1249:
1243:
1236:
1226:
1218:
1211:
1207:
1203:
1193:
1189:
1185:
1179:
1173:
1165:
1161:
1153:
1149:
1145:
1139:
1129:
1122:
1118:
1114:
1108:
1100:
1093:
1083:
1075:
1068:
1064:
1060:
1050:
1043:
1039:
1035:
1029:
1021:
1014:
1004:
996:
992:
988:
982:
972:
968:
964:
958:
951:
943:
937:
927:
920:
916:
912:
906:
895:
891:
867:
850:
840:
836:
832:
828:
810:
809:Given a set
808:
798:
794:
786:
782:
778:
774:
762:
760:
753:
749:
745:
741:
737:
733:
727:
721:
705:
692:
688:
684:
680:
676:
670:
654:
642:
638:
634:
632:
626:
619:
606:
602:
595:
582:
575:
562:
558:
554:
545:
539:
535:
531:
527:
523:
519:
515:
511:
507:
503:
499:
494:
490:
484:
471:
467:
463:
461:
455:
448:
435:
428:
415:
411:
407:
400:
387:
383:
379:
365:
361:
357:
353:
349:
345:
341:
337:
333:
329:
325:
322:
314:
298:
274:
258:
237:
222:
211:
207:
200:
184:
171:
167:
159:
141:
120:
105:
101:
94:
81:
77:
75:
72:Introduction
56:
48:word problem
22:Donald Knuth
17:
15:
5401:Knuth Prize
5045:24 December
3247:We use the
1938:normal form
1913:each class
1871:Consider a
1805:pm(83,151)
1498:f(X,f(0,Y))
1479:f(X,f(Y,Z))
1473:f(f(X,Y),Z)
1156:} ›
5441:Categories
5331:Algorithms
4873:References
4152:), we get
3803:), we get
3610:), we get
3572:), we get
2202:, suppose
2072:generators
1837:generators
1786:rw(134,1)
1748:rw(79,52)
1691:rw(63,52)
1653:pm(46,52)
1615:rw(36,46)
797:and using
581: 1⋅
76:For a set
5288:AMS Euler
5132:MathWorld
4827:−
4811:−
4769:−
4747:−
4710:⟩
4693:−
4677:−
4655:−
4639:−
4598:−
4582:−
4562:⟨
4498:→
4420:→
4367:→
4316:→
4237:→
4052:→
3876:→
3710:→
3388:→
3328:→
3277:→
3231:⟩
3177:∣
3165:⟨
3037:→
2981:≠
2436:overlap.
2260:→
2096:relations
2038:⟩
2032:∣
2026:⟨
1934:canonical
1900:⟩
1894:∣
1888:⟨
1811:See also
1802:i(f(Y,X))
1767:pm(83,6)
1758:f(i(X),0)
1729:pm(3,74)
1710:pm(2,67)
1701:f(i(X),X)
1672:rw(7,52)
1634:pm(2,52)
1596:pm(5,36)
1577:rw(27,1)
1454:f(X,i(X))
1196:} ›
434: 1⋅
390:)
284:of their
280:) is the
244:) is its
147:) is the
127:) is its
41:confluent
39:) into a
33:equations
29:algorithm
5258:Metafont
5245:Software
5034:: 1–30.
3447:(namely
3145:Examples
2050:, where
1558:pm(7,2)
1539:pm(3,2)
1520:pm(2,3)
1501:pm(3,1)
1396:simplify
1392:collapse
1321: ›
1296: ›
1221: ›
1174:Collapse
1132: ›
1078: ›
1053: ›
1030:Simplify
946: ›
930: ›
769:, and a
406: (
370:are the
246:converse
5421:-yllion
5262:MIXAL (
4953:, p. 55
4284:) and (
4146:) and (
3969:) and (
3797:) and (
2138:(e.g.,
1923:, ... }
1682:i(i(X))
1644:i(i(X))
1388:compose
1350:Example
1302:‹
1286:‹
1202:‹
1178:‹
1138:‹
1113:‹
1059:‹
1034:‹
981:‹
957:‹
952:Compose
936:‹
911:‹
871:in the
625:
609:
601:
585:
565:
454:
438:
418:
248:, and (
131:, and (
52:algebra
5006:
4945:
4905:
2869:using
1829:cosets
1720:f(0,Y)
1650:f(0,X)
1606:f(0,X)
1587:f(X,Y)
1549:f(X,0)
1530:f(0,Y)
1492:f(X,Y)
1435:f(X,0)
1424:Source
1394:, and
1384:deduce
1370:, and
1360:f(X,Y)
1282:Deduce
1109:Orient
907:Delete
518:→ 1, (
502:= { 1⋅
344:= 1, (
35:(over
5384:Other
5280:Fonts
5078:(PDF)
5066:(PDF)
5028:(PDF)
4927:(PDF)
1831:of a
1374:for −
1336:is a
1267:) ▻ (
1257:with
1164:>
894:>
835:) ▻ (
815:terms
805:Rules
767:terms
372:group
328:= {1⋅
37:terms
5321:CWEB
5269:MMIX
5107:."
5047:2021
5004:ISBN
4943:ISBN
4903:ISBN
4819:<
4803:<
4797:<
4761:<
4755:<
4739:<
2806:and
2728:and
2602:and
2530:and
2409:and
2352:and
2220:<
2106:<
2074:and
1847:The
1791:165:
1777:i(X)
1772:151:
1753:134:
1625:i(0)
1372:i(X)
1362:for
889:and
885:are
881:and
875:, or
857:>
845:if
304:and
151:of (
16:The
5316:WEB
5264:MIX
5253:TeX
5090:doi
5036:doi
4935:doi
3075:to
3040:min
3011:max
2182:in
1996:i+1
1936:or
1919:, w
1734:83:
1715:79:
1696:74:
1677:67:
1658:64:
1639:63:
1620:60:
1601:52:
1582:46:
1563:36:
1544:27:
1419:Rhs
1412:Lhs
1340:of
1324:if
1247:by
1224:if
1159:if
1081:if
1002:if
542:) }
474:)
320:).
112:, (
5443::
5129:.
5086:23
5084:.
5080:.
5030:.
4941:.
4929:.
3095:.
2282:.
1986:.
1915:{w
1525:7:
1506:6:
1487:5:
1468:3:
1449:2:
1430:1:
1405:Nr
1390:,
1317:,
1314:}
1310:=
1306:∪{
1299:⊢
1292:,
1271:→
1263:→
1252:→
1217:,
1214:}
1210:=
1206:∪{
1199:⊢
1192:→
1188:∪{
1184:,
1152:→
1148:∪{
1144:,
1135:⊢
1128:,
1125:}
1121:=
1117:∪{
1074:,
1071:}
1067:=
1063:∪{
1056:⊢
1049:,
1046:}
1042:=
1038:∪{
995:→
991:∪{
987:,
971:→
967:∪{
963:,
942:,
933:⊢
926:,
923:}
919:=
915:∪{
839:→
831:→
801:.
748:⋅(
744:→
740:)⋅
695:)
687:⋅(
681:R'
641:)⋅
561:)⋅
534:⋅(
530:→
526:)⋅
510:,
506:→
495:E'
466:⋅(
414:)⋅
382:⋅(
368:)}
360:⋅(
356:=
352:)⋅
336:,
332:=
264:∘
190:∘
68:.
54:.
5271:)
5201:"
5197:"
5169:e
5162:t
5155:v
5135:.
5096:.
5092::
5049:.
5038::
5012:.
4951:.
4937::
4911:.
4830:1
4823:y
4814:1
4807:x
4800:y
4794:x
4772:1
4765:y
4758:y
4750:1
4743:x
4736:x
4713:.
4707:1
4704:=
4701:y
4696:1
4689:y
4685:=
4680:1
4673:y
4669:y
4666:=
4663:x
4658:1
4651:x
4647:=
4642:1
4635:x
4631:x
4628:,
4625:x
4622:y
4619:=
4616:y
4613:x
4608:|
4601:1
4594:y
4590:,
4585:1
4578:x
4574:,
4571:y
4568:,
4565:x
4533:)
4530:7
4527:(
4522:.
4510:y
4507:x
4504:y
4501:x
4493:2
4489:x
4483:2
4479:y
4462:)
4459:6
4456:(
4438:2
4434:y
4428:2
4424:x
4417:x
4414:y
4411:x
4408:y
4392:)
4389:2
4386:(
4370:1
4362:3
4358:y
4341:)
4338:1
4335:(
4319:1
4311:3
4307:x
4287:5
4281:4
4271:)
4269:7
4267:(
4261:.
4249:y
4246:x
4243:y
4240:x
4232:2
4228:x
4222:2
4218:y
4190:2
4186:x
4180:2
4176:y
4172:=
4169:y
4166:x
4163:y
4160:x
4149:5
4143:1
4126:3
4122:x
4118:y
4115:x
4112:y
4109:x
4094:)
4092:6
4090:(
4084:.
4070:2
4066:y
4060:2
4056:x
4049:x
4046:y
4043:x
4040:y
4013:2
4009:y
4003:2
3999:x
3995:=
3992:x
3989:y
3986:x
3983:y
3972:5
3966:1
3951:x
3948:y
3945:x
3942:y
3937:3
3933:x
3918:3
3908:)
3906:5
3904:(
3898:.
3884:2
3880:y
3873:x
3870:y
3867:x
3864:y
3861:x
3834:2
3830:y
3826:=
3823:x
3820:y
3817:x
3814:y
3811:x
3800:3
3794:2
3777:3
3773:y
3769:x
3766:y
3763:x
3760:y
3757:x
3742:)
3740:4
3738:(
3732:.
3718:2
3714:x
3707:y
3704:x
3701:y
3698:x
3695:y
3668:2
3664:x
3660:=
3657:y
3654:x
3651:y
3648:x
3645:y
3623:2
3619:x
3607:3
3592:y
3589:x
3586:y
3583:x
3580:y
3569:1
3554:y
3551:x
3548:y
3545:x
3542:y
3537:3
3533:x
3512:y
3509:x
3506:y
3503:x
3500:y
3497:x
3494:=
3489:3
3485:)
3481:y
3478:x
3475:(
3455:x
3433:3
3429:x
3413:)
3411:3
3409:(
3403:.
3391:1
3383:3
3379:)
3375:y
3372:x
3369:(
3352:)
3350:2
3348:(
3331:1
3323:3
3319:y
3301:)
3299:1
3297:(
3280:1
3272:3
3268:x
3243:.
3228:1
3225:=
3220:3
3216:)
3212:y
3209:x
3206:(
3203:=
3198:3
3194:y
3190:=
3185:3
3181:x
3174:y
3171:,
3168:x
3126:R
3106:R
3083:R
3061:2
3057:r
3053:,
3048:1
3044:r
3032:2
3028:r
3024:,
3019:1
3015:r
2989:2
2985:r
2976:1
2972:r
2949:2
2945:r
2941:,
2936:1
2932:r
2909:j
2905:P
2882:i
2878:P
2857:C
2854:B
2851:A
2839:.
2827:B
2824:=
2819:j
2815:P
2794:C
2791:B
2788:A
2785:=
2780:i
2776:P
2755:C
2752:B
2749:A
2746:=
2741:j
2737:P
2716:B
2713:=
2708:i
2704:P
2681:j
2677:P
2654:i
2650:P
2638:.
2626:C
2623:B
2620:=
2615:j
2611:P
2590:B
2587:A
2584:=
2579:i
2575:P
2554:B
2551:A
2548:=
2543:j
2539:P
2518:C
2515:B
2512:=
2507:i
2503:P
2480:j
2476:P
2453:i
2449:P
2422:j
2418:P
2395:i
2391:P
2365:i
2361:Q
2338:i
2334:P
2311:i
2307:Q
2303:=
2298:i
2294:P
2268:i
2264:Q
2255:i
2251:P
2228:i
2224:P
2215:i
2211:Q
2190:R
2168:i
2164:Q
2160:=
2155:i
2151:P
2126:X
2082:R
2058:X
2035:R
2029:X
2004:m
2000:n
1992:i
1958:i
1956:w
1951:k
1949:w
1944:k
1942:w
1929:k
1927:w
1921:2
1917:1
1897:R
1891:X
1885:=
1882:M
1799:=
1780:=
1761:=
1742:=
1739:Y
1723:=
1707:0
1704:=
1688:X
1685:=
1669:Y
1666:=
1647:=
1631:0
1628:=
1612:X
1609:=
1590:=
1571:=
1568:X
1552:=
1533:=
1517:0
1514:=
1495:=
1476:=
1460:0
1457:=
1441:X
1438:=
1376:X
1368:Y
1366:+
1364:X
1342:R
1334:)
1332:t
1330:,
1328:s
1326:(
1319:R
1312:t
1308:s
1304:E
1294:R
1288:E
1275:)
1273:r
1269:l
1265:t
1261:s
1259:(
1254:r
1250:l
1244:u
1237:R
1232:⟶
1227:s
1219:R
1212:t
1208:u
1204:E
1194:t
1190:s
1186:R
1180:E
1166:t
1162:s
1154:t
1150:s
1146:R
1140:E
1130:R
1123:t
1119:s
1115:E
1101:u
1094:R
1089:⟶
1084:t
1076:R
1069:u
1065:s
1061:E
1051:R
1044:t
1040:s
1036:E
1022:u
1015:R
1010:⟶
1005:t
997:u
993:s
989:R
983:E
973:t
969:s
965:R
959:E
944:R
938:E
928:R
921:s
917:s
913:E
899:.
896:r
892:t
883:l
879:s
868:l
861:e
851:s
843:)
841:r
837:l
833:t
829:s
827:(
811:E
799:R
795:E
787:R
783:E
779:E
775:R
763:E
756:)
754:z
752:⋅
750:y
746:x
742:z
738:y
736:⋅
734:x
732:(
728:b
722:R
718:⟵
715:⁎
711:∘
706:R
702:⟶
699:⁎
693:b
691:⋅
689:a
685:a
677:b
671:R
667:⟵
664:⁎
660:∘
655:R
651:⟶
648:⁎
643:b
639:a
637:⋅
635:a
627:b
620:R
616:⟵
613:⁎
607:b
603:b
596:R
592:⟶
589:⁎
583:b
576:R
572:⟶
569:⁎
563:b
559:a
557:⋅
555:a
553:(
546:E
540:z
538:⋅
536:y
532:x
528:z
524:y
522:⋅
520:x
516:x
514:⋅
512:x
508:x
504:x
500:R
491:b
485:E
481:⟷
478:⁎
472:b
470:⋅
468:a
464:a
456:b
449:E
445:⟷
442:⁎
436:b
429:E
425:⟷
422:⁎
416:b
412:a
410:⋅
408:a
401:E
397:⟷
394:⁎
388:b
386:⋅
384:a
380:a
366:z
364:⋅
362:y
358:x
354:z
350:y
348:⋅
346:x
342:x
340:⋅
338:x
334:x
330:x
326:E
315:R
311:⟵
308:⁎
299:R
295:⟶
292:⁎
288:(
275:R
271:⟵
268:⁎
259:R
255:⟶
252:⁎
238:R
233:⟵
223:R
218:⟶
212:R
208:R
201:R
197:⟵
194:⁎
185:R
181:⟶
178:⁎
174:(
168:R
160:E
155:⟶
142:E
138:⟷
135:⁎
121:E
116:⟶
106:E
102:E
95:E
91:⟷
88:⁎
84:(
78:E
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.