PATCH Graphs: An efficient data structure for completion of finitely presented groups

  • Christopher Lynch
  • Polina Strogova
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1138)


Based on a new data structure called PATCH Graph, an efficient completion procedure for finitely presented groups is described. A PATCH Graph represents rules and their symmetrized forms as cycles in a Cayley graph structure. Completion is easily performed directly on the graph, and structure sharing is enforced. The structure of the graph allows us to avoid certain redundant inferences. The PATCH Graph data structure and inference rules complement other extensions of Knuth-Bendix completion for finitely presented groups.


Inference Rule Cayley Graph Symmetrize Form Critical Pair Initial Vertex 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BO93]
    R. V. Book and F. Otto. String-Rewriting Sytsems. Springer-Verlag, 1993.Google Scholar
  2. [Büc79]
    Hans Bücken. Reduction-systems and small cancellation theory. In Proceedings of 4th Workshop on Automated Deduction, pages 53–59, 1979.Google Scholar
  3. [DJ90]
    N. Dershowitz and J.-P. Jouannaud. Handbook of Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 244–320. Elsevier Science Publishers B. V. (North-Holland), 1990. Also as: Research report 478, LRI.Google Scholar
  4. [EHR91]
    D. B. A. Epstein, D. F. Holt, and S. Rees. The use of knuth-bendix methods to solve the word problem in authomatic groups. Journal of Symbolic Computation, 12:397–414, 1991.Google Scholar
  5. [FKS94]
    D. Fortin, C. Kirchner, and P. Strogova. Routing in Regular Networks Using Rewriting. In J. Slaney, editor, Proceedings of the CADE international workshop on automated reasoning in algebra (ARIA), pages 5–8, June 1994.Google Scholar
  6. [Gil79]
    R. H. Gilman. Presentations of groups and monoids. J. of Algebra, 57:544–554, 1979.CrossRefGoogle Scholar
  7. [HR89]
    D. Holt and S. Rees. Testing for isomorphism between finitely presented groups. In Proceedings of the Conference on Groups and Combinatorics, Cambridge, 1989. Cambridge University Press.Google Scholar
  8. [KB70]
    Donald E. Knuth and P. B. Bendix. Simple word problems in universal algebras. In J. Leech, editor, Computational Problems in Abstract Algebra, pages 263–297. Pergamon Press, Oxford, 1970.Google Scholar
  9. [KZ88]
    D. Kapur and H. Zhang. RRL: A rewrite rule laboratory. In Proceedings 9th International Conference on Automated Deduction, Argonne (Ill. USA), volume 310 of Lecture Notes in Computer Science, pages 768–769. Springer-Verlag, 1988.Google Scholar
  10. [LC86]
    Ph. Le Chenadec. Canonical Forms in Finitely Presented Algebras. John Wiley & Sons, 1986.Google Scholar
  11. [LS95]
    Christopher Lynch and Polina Strogova. Sour graphs for efficient completion. Technical Report 95-R-343, CRIN, 1995.Google Scholar
  12. [Lyn95]
    Christopher Lynch. Paramodulation without duplication. In Dexter Kozen, editor, Proceedings of LICS'95, San Diego, June 1995.Google Scholar
  13. [Mar93]
    C. Marché. Réécriture modulo une théorie présentée par un système convergent et décidabilité du problème du mot dans certaines classes de théories équationnelles. Thèse de Doctorat d'Université, Université de Paris-Sud, Orsay (France), October 1993.Google Scholar
  14. [Mar96]
    U. Martin. Theorem proving with group presentations: examples and questions. In Proceedings of CADE-13, 1996. To appear.Google Scholar
  15. [McC94]
    W. W. McCune. Otter 3.0: Reference manual and guide. Technical Report 6, Argonne National Laboratory, 1994.Google Scholar
  16. [MNO91]
    K. Madlener, P. Narendran, and F. Otto. A specialized completion procedure for monadic string-rewriting systems presenting groups. In Proceedings 18th ICALP Conference, Madrid (Spain), volume 516 of Lecture Notes in Computer Science, pages 279–290. Springer-Verlag, 1991.Google Scholar
  17. [Sim87]
    C. C. Sims. Verifying nilpotence. Journal of Symbolic Computation, 3:231–247, 1987.Google Scholar
  18. [Zha92]
    H. Zhang. Herky: High-performance rewriting techniques in rrl. In D. Kapur, editor, Proceedings of 1992 International Conference of Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 696–700. Springer-Verlag, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Christopher Lynch
    • 1
  • Polina Strogova
    • 2
  1. 1.Technopôle de Nancy-BraboisINRIA Lorraine-CRINVillers-lès-Nancy CedexFrance
  2. 2.Technopôle de Nancy-BraboisINRIA Lorraine-CRIN and INRIA RocquencourtVillers-lès-Nancy CedexFrance

Personalised recommendations