31:
491:
532:
106:
561:
47:
525:
551:
51:
30:
131:
518:
556:
205:
94:
388:
127:
227:
123:
502:
498:
428:
453:
449:
55:
17:
545:
433:
416:
216:
460:. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.
352:
322:
291:
280:
223:
183:
165:
86:
71:
135:
490:
417:"A Complete Proof of Correctness of the Knuth–Bendix Completion Algorithm"
141:
119:
67:
471:
Dershowitz, Jouannaud (1990), sect.5.4, p. 278; somewhat sloppy,
29:
340:
i.e. irreflexive, transitive, and well-founded binary relation
475:
is required to be a "terminating rewrite relation" there.
506:
230:
of (≤). In particular, (<) itself is well-founded.
526:
8:
533:
519:
432:
407:
240:
42:related by the encompassment preorder.
7:
487:
485:
27:Term ordering in abstract rewriting
505:. You can help Knowledge (XXG) by
142:corresponding equivalence relation
25:
107:Knuth–Bendix completion algorithm
489:
215:The union of any well-founded
34:Triangle diagram of two terms
1:
434:10.1016/0022-0000(81)90002-7
48:theoretical computer science
226:, where (<) denotes the
578:
484:
462:Here:sect.2.1, p. 250
52:automated theorem proving
166:equality modulo renaming
105:It is used e.g. in the
562:Computer science stubs
43:
18:Encompassment preorder
206:substitution instance
95:substitution instance
33:
421:J. Comput. Syst. Sci
415:Gerard Huet (1981).
118:Encompassment is a
50:, in particular in
228:irreflexive kernel
70:(≤) on the set of
44:
552:Rewriting systems
514:
513:
16:(Redirected from
569:
535:
528:
521:
499:computer science
493:
486:
476:
469:
463:
461:
445:
439:
438:
436:
412:
395:
338:
332:
323:constant symbols
303:
297:
281:variable symbols
245:
74:, is defined by
21:
577:
576:
572:
571:
570:
568:
567:
566:
542:
541:
540:
539:
482:
480:
479:
470:
466:
458:Rewrite Systems
454:Jan van Leeuwen
450:J.-P. Jouannaud
448:N. Dershowitz,
447:
446:
442:
414:
413:
409:
404:
399:
398:
366:
357:
339:
335:
304:
300:
292:function symbol
246:
242:
237:
222:with (<) is
115:
28:
23:
22:
15:
12:
11:
5:
575:
573:
565:
564:
559:
554:
544:
543:
538:
537:
530:
523:
515:
512:
511:
494:
478:
477:
464:
440:
406:
405:
403:
400:
397:
396:
367:for all terms
362:
353:
333:
305:since neither
298:
271:) ≤
255:) ≤
239:
238:
236:
233:
232:
231:
213:
191:
169:
138:
132:anti-symmetric
114:
111:
103:
102:
56:term rewriting
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
574:
563:
560:
558:
555:
553:
550:
549:
547:
536:
531:
529:
524:
522:
517:
516:
510:
508:
504:
501:article is a
500:
495:
492:
488:
483:
474:
468:
465:
459:
455:
451:
444:
441:
435:
430:
426:
422:
418:
411:
408:
401:
394:
390:
386:
382:
378:
374:
370:
365:
361:
356:
351:
347:
343:
337:
334:
331:
327:
324:
321:for distinct
320:
317: ≤
316:
312:
309: ≤
308:
302:
299:
296:
293:
289:
285:
282:
278:
274:
270:
266:
262:
258:
254:
250:
244:
241:
234:
229:
225:
221:
218:
217:rewrite order
214:
211:
207:
203:
199:
196: ≤
195:
192:
189:
185:
181:
177:
174: ≤
173:
170:
167:
163:
160: ≤
159:
156: ≤
155:
151:
148: ~
147:
144:, defined by
143:
139:
137:
133:
129:
125:
121:
117:
116:
112:
110:
108:
100:
96:
92:
88:
84:
81: ≤
80:
77:
76:
75:
73:
69:
65:
64:encompassment
61:
57:
53:
49:
41:
38: ≤
37:
32:
19:
557:Order theory
507:expanding it
496:
481:
472:
467:
457:
443:
427:(1): 11–21.
424:
420:
410:
392:
389:substitution
384:
380:
379:, each path
376:
372:
368:
363:
359:
354:
349:
345:
341:
336:
329:
325:
318:
314:
310:
306:
301:
294:
287:
283:
276:
272:
268:
264:
260:
256:
252:
248:
243:
224:well-founded
219:
209:
201:
197:
193:
187:
179:
175:
171:
161:
157:
153:
149:
145:
104:
98:
90:
82:
78:
63:
59:
45:
39:
35:
387:, and each
247:since both
60:containment
546:Categories
402:References
344:such that
130:, but not
128:transitive
113:Properties
200:whenever
178:whenever
124:reflexive
452:(1990).
348:implies
120:preorder
68:preorder
456:(ed.).
184:subterm
122:, i.e.
87:subterm
391:
290:and a
279:) for
263:) and
134:, nor
58:, the
497:This
235:Notes
204:is a
182:is a
164:, is
136:total
93:is a
85:if a
72:terms
62:, or
503:stub
313:nor
140:The
126:and
54:and
429:doi
383:of
346:sRt
208:of
186:of
152:if
97:of
89:of
46:In
548::
425:23
423:.
419:.
375:,
371:,
358:R
328:,
286:,
109:.
66:,
534:e
527:t
520:v
509:.
473:R
437:.
431::
393:σ
385:u
381:p
377:u
373:t
369:s
364:p
360:u
355:p
350:u
342:R
330:b
326:a
319:a
315:b
311:b
307:a
295:f
288:y
284:x
277:x
275:(
273:f
269:y
267:(
265:f
261:y
259:(
257:f
253:x
251:(
249:f
220:R
212:.
210:s
202:t
198:t
194:s
190:.
188:t
180:s
176:t
172:s
168:.
162:s
158:t
154:s
150:t
146:s
101:.
99:s
91:t
83:t
79:s
40:t
36:s
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
