A case study of completion modulo distributivity and Abelian groups

  • Hantao Zhang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 690)

Abstract

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.

Keywords

Coherence Tate Alan 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Anantharaman, S., Hsiang, J.: (1990) Automated proofs of the Moufang identities in alternative rings. J. of Automated Reasoning 6 79–109.CrossRefMATHMathSciNetGoogle Scholar
  2. [2]
    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
  3. [3]
    Dershowitz, N., Jouannaud J.P.: (1990) Rewriting systems. In Leuven, V. (ed.): Handbook of Theoretical Computer Science. North Holland.Google Scholar
  4. [4]
    Jouannaud, J.P., Kirchner, H.: (1986) Completion of a set of rules modulo a set of equations. SIAM J. on Computing, 15:1155–1194.CrossRefMATHMathSciNetGoogle Scholar
  5. [5]
    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
  6. [6]
    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
  7. [7]
    Peterson, G.L., Stickel, M.E.: (1981) Complete sets of reductions for some equational theories. J. ACM 28:2 233–264.CrossRefMATHMathSciNetGoogle Scholar
  8. [8]
    Stevens, R.L.: (1987) Some Experiments in nonassociative ring theory with an automated theorem prover. J. of Automated Reasoning 3 211–221.CrossRefMATHMathSciNetGoogle Scholar
  9. [9]
    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
  10. [10]
    Wang, T.C.: (1987) Case studies of Z-module reasoning: proving benchmark theorems from ring theory. J. of Automated Reasoning 3 437–451.MATHGoogle Scholar
  11. [11]
    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
  12. [12]
    Wang, T.C., Stevens, R.L.: (1989) Solving open problems in right alternative rings with Z-module reasoning. J. of Automated Reasoning 5 141–165.CrossRefMATHMathSciNetGoogle Scholar
  13. [13]
    Zhang, H.: (1991) Criteria of critical pair criteria: a practical approach and a comparative study. To appear in J. of Automated Reasoning.Google Scholar
  14. [14]
    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
  15. [15]
    Zhevlakov, K.A., at al: (1982) Rings that are nearly associative (translated by H.F. Smith from Russia). Academic Press, New York.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Hantao Zhang
    • 1
  1. 1.University of IowaIowaUSA

Personalised recommendations