Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Artificial Intelligence and Symbolic Mathematical Computation (AISMC 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1138))

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. V. Book and F. Otto. String-Rewriting Sytsems. Springer-Verlag, 1993.

    Google Scholar 

  2. Hans Bücken. Reduction-systems and small cancellation theory. In Proceedings of 4th Workshop on Automated Deduction, pages 53–59, 1979.

    Google Scholar 

  3. 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. 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. 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. R. H. Gilman. Presentations of groups and monoids. J. of Algebra, 57:544–554, 1979.

    Article  Google Scholar 

  7. 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. 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. 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. Ph. Le Chenadec. Canonical Forms in Finitely Presented Algebras. John Wiley & Sons, 1986.

    Google Scholar 

  11. Christopher Lynch and Polina Strogova. Sour graphs for efficient completion. Technical Report 95-R-343, CRIN, 1995.

    Google Scholar 

  12. Christopher Lynch. Paramodulation without duplication. In Dexter Kozen, editor, Proceedings of LICS'95, San Diego, June 1995.

    Google Scholar 

  13. 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. U. Martin. Theorem proving with group presentations: examples and questions. In Proceedings of CADE-13, 1996. To appear.

    Google Scholar 

  15. W. W. McCune. Otter 3.0: Reference manual and guide. Technical Report 6, Argonne National Laboratory, 1994.

    Google Scholar 

  16. 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. C. C. Sims. Verifying nilpotence. Journal of Symbolic Computation, 3:231–247, 1987.

    Google Scholar 

  18. 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 

Download references

Author information

Authors and Affiliations

  1. Technopôle de Nancy-Brabois, INRIA Lorraine-CRIN, B.P. 101, 54602, Villers-lès-Nancy Cedex, France

    Christopher Lynch

  2. Technopôle de Nancy-Brabois, INRIA Lorraine-CRIN and INRIA Rocquencourt, B.P. 101, 54602, Villers-lès-Nancy Cedex, France

    Polina Strogova

Authors
  1. Christopher Lynch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Polina Strogova
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jacques Calmet John A. Campbell Jochen Pfalzgraf

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lynch, C., Strogova, P. (1996). PATCH Graphs: An efficient data structure for completion of finitely presented groups. In: Calmet, J., Campbell, J.A., Pfalzgraf, J. (eds) Artificial Intelligence and Symbolic Mathematical Computation. AISMC 1996. Lecture Notes in Computer Science, vol 1138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61732-9_57

Download citation

  • DOI: https://doi.org/10.1007/3-540-61732-9_57

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61732-7

  • Online ISBN: 978-3-540-70740-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation