Some experiments with a completion theorem prover. (English) Zbl 0748.68071
This paper is intended to show how an automatic theorem prover, which uses the completion algorithm, can solve problems in algebra. The results have been obtained using version 2.4 of the prover REVE (one of the most important author is Pierre Lescanne).
The completion algorithm takes as input a set of equations and rules and an ordering, and constructs new rules by ordering equations, and new equations by computing critical pairs. A complete (terminating and confluent) set of rules equivalent to a given set of equations gives a solution to the word problem in the variety which is defined by the equations. Of course, since not all algebraic systems have a decidable word problem, there are systems for which no finite complete set of rules can be found.
The authors show how REVE solves a series of standard “test problems”: homomorphisms and automorphisms of groups, alternative axiomatization of groups, ternary algebra, non-associative rings, the Fibonacci groups. There are 18 examples, each of them with the input equations and with a complete set of rewrite rules output.
Some cases, where the completion algorithm diverges, are presented, especially when the operator precedence is changed.
The completion algorithm takes as input a set of equations and rules and an ordering, and constructs new rules by ordering equations, and new equations by computing critical pairs. A complete (terminating and confluent) set of rules equivalent to a given set of equations gives a solution to the word problem in the variety which is defined by the equations. Of course, since not all algebraic systems have a decidable word problem, there are systems for which no finite complete set of rules can be found.
The authors show how REVE solves a series of standard “test problems”: homomorphisms and automorphisms of groups, alternative axiomatization of groups, ternary algebra, non-associative rings, the Fibonacci groups. There are 18 examples, each of them with the input equations and with a complete set of rewrite rules output.
Some cases, where the completion algorithm diverges, are presented, especially when the operator precedence is changed.
Reviewer: D.Tătar (Cluj)
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 68Q42 | Grammars and rewriting systems |
References:
| [1] | Anantharaman, S.; Hsiang, J.; Msali, J., SbReve2: A Term Rewriting Laboratory with (AC-)Unfailing Completion, (Dershowits, N., 3rd Inter. Conf., RTA-89, Proceedings. 3rd Inter. Conf., RTA-89, Proceedings, Lecture Notes in Computer Science (1989)), 533-537, Springer 355 |
| [2] | Bergman, G., The diamond lemma for ring theory, Adv Math, 29, 178-218 (1978) · Zbl 0326.16019 |
| [3] | Buchberger, B., History and Basic Features of the Critical-Pair Completion Procedure, J. Symbolic Computation, 3, 3-38 (1987) · Zbl 0645.68094 |
| [4] | Brown, K., The Geometry of Rewriting Systems (1989), Cornell University, preprint |
| [5] | Brown, R., Higher Dimensional Group Theory, (Proceedings of the Conference on Topology in Low Dimensions. Proceedings of the Conference on Topology in Low Dimensions, Bangor. Proceedings of the Conference on Topology in Low Dimensions. Proceedings of the Conference on Topology in Low Dimensions, Bangor, London Mathematical Society Lecture Note Series 48 (1979)) · Zbl 0484.55007 |
| [6] | Canon, J., A Language for Group Theory (July 1982), Dept. of Mathematics, University of Sydney: Dept. of Mathematics, University of Sydney Australia |
| [7] | Dershowits, N., Termination of Rewriting, Journal of Symbolic Computation, 3, 69-116 (1987) · Zbl 0637.68035 |
| [8] | Dick, A. J.J.; Kahnus, J. R., (ERIL User’s Manual (1988), Rutherford Appleton Laboratory), Technical Report RAL-88-055 |
| [9] | D. B. A. Epstein, D. F. Holt and S. E. Rees, The use of Knuth-Bendix methods to solve the word problem in automatic groups, to appear, Journal of Symbolic Computation; D. B. A. Epstein, D. F. Holt and S. E. Rees, The use of Knuth-Bendix methods to solve the word problem in automatic groups, to appear, Journal of Symbolic Computation · Zbl 0779.20017 |
| [10] | Garland, S.; Guttag, J., The Larch Prover, Lecture Notes in Computer Science, (Dershowits, N., 3rd Inter. Conf., RTA-89, Proceedings (1989)), Springer 355 · Zbl 1503.68290 |
| [11] | Hall, M., The Theory of Groups (1959), Macmillan · Zbl 0084.02202 |
| [12] | Hermann, M.; Kirchner, C.; Kirchner, H., Implementations of Term Rewriting Systems, Computer Journal, 34, 20-33 (1991) |
| [13] | Howie, J.; Pride, S., The word problem for one-relator semigroups, (Math Proc Cam Phil Soc, 99 (1986)), 33-44 · Zbl 0584.20045 |
| [14] | Huet, G.; Oppen, D., Equations and Rewrite Rules — a survey, (Book, R., Formal Languages: Perspectives and Open Problems (1980), Academic Press) |
| [15] | Jackson, D. A., Some one relator semigroups with soluble word problems, (Math Proc Cam Phil Soc, 99 (1986)), 433-434 · Zbl 0601.20052 |
| [16] | Jantsen, M., Confluent String Rewriting, (EATCS Monographs on Theoretical Computer Science, Vol. 14 (1988), Springer) · Zbl 1097.68572 |
| [17] | Johnson, D. L., Topics in the theory of group presentations, London Mathematical Society Lecture Note Series, 42 (1979) · Zbl 0437.20026 |
| [18] | Kapur, D.; Zhang, H., A case study of the completion procedure: proving ring commutstivity problems, (Lasses; Plotkin, Tech Report SUNY at Albany (May 1989), Festschrift for Alan Robinson), to appear |
| [19] | Knuth, D.; Bendix, P., Simple Word Problems in Universal Algebras, (Leech, J., Computational Problems in Abstract Algebra (1970), Pergamon Press) · Zbl 0188.04902 |
| [20] | Kapur, D.; Zhang, H., Proving equivalence of different axiomatisations of free groups, Journal of Automated Reasoning, 331-352 (1988) · Zbl 0654.68102 |
| [21] | Kapur, D.; Zhang, H., An Overview of the Rewrite Rule Laboratory (RRL), (Dershowits, N., 3rd Inter. Conf., RTA-89, Proceedings. 3rd Inter. Conf., RTA-89, Proceedings, Lecture Notes in Computer Science, 355 (1989), Springer) |
| [22] | Kapur, D.; Sivakumar, G.; Zhang, H., RRL: A Rewrite Rule Laboratory, (8th Intl. Conf. on Automated Deduction. 8th Intl. Conf. on Automated Deduction, Lecture Notes in Computer Science, 230 (1986), Springer) |
| [23] | Le Chenadec, P., Canonical Forms in Finitely presented Algebras, (7th International Conference on Automated Deduction. 7th International Conference on Automated Deduction, Lecture Notes in Computer Science, 170 (1984), Springer) · Zbl 0547.03028 |
| [24] | Lescanne, P., Term Rewriting Systems and Algebra, (7th International Conference on Automated Deduction. 7th International Conference on Automated Deduction, Lecture Notes in Computer Science, 170 (1984), Springer) · Zbl 0546.68079 |
| [25] | Lusk, E.; Overbeek, R., The Automated Reasoning System ITP, Argonne National laboratory ANL-84-27 (1984) |
| [26] | Martin, U., Doing Algebra with REVE (1986), University of Manchester, Research Report |
| [27] | Newman, M. F., Proving a group infinite, ((1988), Department of Mathematical Sciences, IAS, Australian National University), Ressearch report 26 · Zbl 0662.20023 |
| [28] | Neumann, B. H., An essay on free products with amalgamations, Phil Trans Royal Soc London Ser A, 246, 503-554 (1954) · Zbl 0057.01702 |
| [29] | Neumann, B. H., Another single law for groups, hBull Austr Math Soc, 23, 81-102 (1981) · Zbl 0581.20003 |
| [30] | Neumann, B. H., (seminar at the University of Oxford (May 1986)) |
| [31] | Sims, C. C., Verifying Nilpotence, Journal of Symbolic Computation, 3, 231-247 (1987) · Zbl 0626.68034 |
| [32] | Stevens, R. L., Some experiments in non-associative ring theory with an automated theorem prover, Journal of Automated Reasoning, 3, 211-221 (1987) · Zbl 0648.17001 |
| [33] | Woo, L., Automated Reasoning: 33 Basic Research Problems (1988), Prentice Hall · Zbl 0663.68102 |
| [34] | Woo, L.; Winker, S., Open questions solved with the assistance of AURA, Contemporary Mathematics, 29, 73-88 (1984) · Zbl 0566.68076 |
| [35] | Zhang, H.; Kapur, D., Unnecessary inferences in associative-commutative completion procedures, J Math System Theory, 23, 175-206 (1990) · Zbl 0707.68071 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
