Term rewriting systems and algebra. (English) Zbl 0546.68079
Automated deduction, Proc. 7th int. Conf., Napa/Calif. 1984, Lect. Notes Comput. Sci. 170, 166-174 (1984).
[For the entire collection see Zbl 0537.00025.]
The author shows, by means of examples taken essentially from group theory, how the system REVE can be directed to increase the effectiveness of the Knuth-Bendix completion algorithm (KBP). The main ideas concern the use of the Recursive Decomposition Ordering with Status, the iteration of the KBP (that is, after a failure, KBP can be restarded with the input produced by the previous iteration) and the use of KBP for generation of ”useful” consequences of an input set of equations, instead of using KBP to produce directly the desired noetherian set of rules.
The author shows, by means of examples taken essentially from group theory, how the system REVE can be directed to increase the effectiveness of the Knuth-Bendix completion algorithm (KBP). The main ideas concern the use of the Recursive Decomposition Ordering with Status, the iteration of the KBP (that is, after a failure, KBP can be restarded with the input produced by the previous iteration) and the use of KBP for generation of ”useful” consequences of an input set of equations, instead of using KBP to produce directly the desired noetherian set of rules.
Reviewer: J.Toader
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 20F10 | Word problems, other decision problems, connections with logic and automata (group-theoretic aspects) |
