A case study of completion modulo distributivity and Abelian groups
We propose an approach for building equational theories with the objective of improving the performance of the completion procedure, even though there exist canonical rewrite systems for these theories. As a test case of our approach, we show how to build the free Abelian groups and distributivity laws in the completion procedure. The empirical results of our experiment on proving many identities in alternative rings show clearly that the gain of this approach is substantial. More than 30 identities which are valid in any alternative ring are taken from the book “Rings that are nearly associative” by K.A. Zhevlakov et al., and include the Moufang identities and the skew-symmetry of the Kleinfeld function. The proofs of these identities are obtained by Herky, a descendent of RRL and a high-performance rewriting-based theorem prover.
KeywordsAbelian Group Theorem Prover Automate Reasoning Free Abelian Group Polynomial Term
Unable to display preview. Download preview PDF.
- Anantharaman, S., Hsiang, J., Mzali, J.: (1989) SbReve2: A term rewriting laboratory with (AC)-unfailing completion. Proc. of the third International Conference on Rewriting Techniques and its Applications (RTA-89). Lecture Notes in Computer Science, Vol. 355, Springer-Verlag, Berlin.Google Scholar
- Dershowitz, N., Jouannaud J.P.: (1990) Rewriting systems. In Leuven, V. (ed.): Handbook of Theoretical Computer Science. North Holland.Google Scholar
- Kapur, D., Zhang, H.: (1989) An overview of RRL: Rewrite Rule Laboratory. Proc. of the third International Conference on Rewriting Techniques and its Applications (RTA-89). Lecture Notes in Computer Science, Vol. 355, Springer-Verlag, Berlin, 513–529.Google Scholar
- Kapur, D., Zhang, H.: (1991) A case study of the completion procedure: Proving ring commutativity problems. In J.-L. Lassez and G. Plotkin (eds.): Computational Logic: Essays in Honor of Alan Robinson, MIT Press, Cambridge, MA.Google Scholar
- Stevens, R.L.: (1988) Challenge problems from nonassociative rings for theorem provers. Proc. of 9th Conference on Automated Deduction, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Vol. 230. pp. 730–734.Google Scholar
- Wang, T.C.: (1988) Elements of Z-module reasoning. Proc. of 9th Conference on Automated deduction, Lecture Notes in Computer Science, Springer-Verlag, Berlin, Vol. 230. pp. 21–40.Google Scholar
- Zhang, H.: (1991) Criteria of critical pair criteria: a practical approach and a comparative study. To appear in J. of Automated Reasoning.Google Scholar
- Zhang, H.: (1991) Herky: High performance rewriting in RRL. In Kapur, D.: (ed.): Proc. of 1992 International Conference of Automated Deduction. Saratoga, NY. Lecture Notes in Artificial Intelligence, 607, Springer-Verlag, pp. 696–700.Google Scholar
- Zhevlakov, K.A., at al: (1982) Rings that are nearly associative (translated by H.F. Smith from Russia). Academic Press, New York.Google Scholar