Skip to main content
SpringerLink
Log in

A new approach to general E-unification based on conditional rewriting systems

  • Applications to Logic Programming, Normalization Strategies and Unification
  • Conference paper
  • First Online:
Conditional Term Rewriting Systems (CTRS 1992)

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

Included in the following conference series:

  • 154 Accesses

Abstract

Using strictly resolvent conditional rewriting presentations of equational theories leads to a new transformation rule. This rule defines an unifying framework for the existing topmost approaches to E-unification. Thus the development of common formal optimizations and implementation techniques is possible. Moreover, new algorithms can be expressed with this rule. For example, presentations based on different kinds of conditions lead to E-unification algorithms the behavior of which depends on the axiom applied. We also present the main ideas of an efficient E-unification algorithm based on presentations the conditions of which contain only E-unification problems between variables.

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. F. Baader and K.U. Schulz. Unification in the union of disjoint equational theories: Combining decision procedures. In Proceedings of the 11th Conference on Automated Deduction, pages 50–65. Springer-Verlag, LNAI 607, 1992.

    Google Scholar 

  2. T. Boy de la Tour, R. Caferra, and G. Chaminade. Some tools for an inference laboratory (ATINF). In Proceedings of the 9th Conference on Automated Deduction, pages 744–745. Springer-Verlag, LNCS 310, 1988.

    Google Scholar 

  3. H. Chen, J. Hsiang, and H.-C. Kong. On finite representation of infinite sequences of terms. In Proceedings of the 2nd international Conditional and Typed Rewriting Systems workshop, pages 100–114. Springer-Verlag, LNCS 516, 1990.

    Google Scholar 

  4. H. Comon, K. Haberstrau, and J.-P. Jouannaud. Decidable problems in shallow equational theories. In Proceeding of the 7th IEEE Symposium on Logic in Computer Science, 1991.

    Google Scholar 

  5. J. Corbin and M. Bidoit. A rehabilitation of Robinson's unification algorithm. In R. Mason, editor, Proceedings of the IFIP'83, pages 909–914, 1983.

    Google Scholar 

  6. M. Davis. The prehistory and early history of automated deduction. In J. Siekmann and G. Wrighston, editors, Automation of Reasoning 1, Classical Papers on Computational Logic 1957–1966. Springer-Verlag, 1983.

    Google Scholar 

  7. B. Delsart. General E-unification: A realistic approach. Presented at UNIF'91, 1991. (extended abstract).

    Google Scholar 

  8. B. Delsart. Efficient E-unification algorithms. Technical report, INPG, 1992.

    Google Scholar 

  9. N. Dershowitz and J.-P. Jouannaud. Hanbook on Theoretical Computer Science, volume B, chapter 6: Rewrite Systems, pages 243–320. J. van Leeuwen (ed.), 1990.

    Google Scholar 

  10. N. Dershowitz and J.-P. Jouannaud. Notations for rewriting. EATCS, 43:162–172, 1991.

    Google Scholar 

  11. D. Dougherty and P. Johann. An improved general E-unification method. In Proceedings of the 10th Conference on Automated Deduction, pages 261–275. Springer-Verlag, LNCS 449, 1990.

    Google Scholar 

  12. M. Fay. First order unification in equational theories. In Proceedings of the 4th Workshop on Automated Deduction, pages 162–167, 1979.

    Google Scholar 

  13. J.H. Gallier and W. Snyder. A general complete E-unification procedure. In Proceeding of the 2nd Conference on Rewrite Techniques and Applications, pages 216–227. Springer-Verlag, LNCS 256, 1987.

    Google Scholar 

  14. J.H. Gallier and W. Snyder. Complete sets of transformations for general E-unification. Theoretical Computer Science, 67(2,3):203–260, 1989.

    Google Scholar 

  15. J. Herbrand. Recherche sur la théorie de la démonstration, 1930. Thèse de doctorat, Université de Paris.

    Google Scholar 

  16. A. Herold. Combination of unification algorithms. In Proceedings of the 8th Conference on Automated Deduction, pages 450–469. Springer-Verlag, LNCS 230, 1986.

    Google Scholar 

  17. G. Huet. Résolution d'équations dans les langages d'ordre 1,2,...,∞. Thèse d'Etat, Université de Paris, 1976.

    Google Scholar 

  18. J.-M. Hullot. Canonical forms and unification. In Proceedings of the 5th Conference on Automated Deduction, pages 318–334. Springer-Verlag, LNCS 87, 1980.

    Google Scholar 

  19. J.-P. Jouannaud and C. Kirchner. Solving equations in abstract algebras: A rule-based survey of unification. Technical Report 561, LRI, 1990.

    Google Scholar 

  20. C. Kirchner. Computing unification algorithms. In Proceedings of the first IEEE Symposium on Logic in Computer Science, pages 206–216, 1986.

    Google Scholar 

  21. H. Kirchner. Schematization of infinite sets of rewrite rules generated by divergent completion processes. Theoretical Computer Science, 67:303–332, 1989.

    Google Scholar 

  22. H. Kirchner and M. Hermann. Meta-rule synthesis for crossed rewrite systems. In Proceedings of the 2nd international Conditional and Typed Rewriting Systems workshop, pages 143–154. Springer-Verlag, LNCS 516, 1990.

    Google Scholar 

  23. A. Martelli and U. Montanari. An efficient unification algorithm. ACM Transaction on Programming Languages And Systems, 4(2):258–282, 1982.

    Google Scholar 

  24. W. Nutt, P. Rety, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7(3,4):295–318, 1989.

    Google Scholar 

  25. M.S. Paterson and M.N. Wegman. Linear unification. Journal of Computer Systems, Sciences, 16:158–167, 1978.

    Google Scholar 

  26. P. Rety. Improving basic narrowing. In Proceedings of the 2nd Conference on Rewriting Techniques and Applications, pages 226–241. Springer-Verlag, LNCS 256, 1987.

    Google Scholar 

  27. A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the Association for Computing Machinery, 12(1):23–41, 1965.

    Google Scholar 

  28. M. Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. Seki report sr-87-16, University of Kaiserslauterm, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut IMAG, LIFIA, 46 Avenue Felix Viallet, 38031, Grenoble, France

    Bertrand Delsart

Authors
  1. Bertrand Delsart
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Michaël Rusinowitch Jean-Luc Rémy

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Delsart, B. (1993). A new approach to general E-unification based on conditional rewriting systems. In: Rusinowitch, M., Rémy, JL. (eds) Conditional Term Rewriting Systems. CTRS 1992. Lecture Notes in Computer Science, vol 656. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56393-8_38

Download citation

  • DOI: https://doi.org/10.1007/3-540-56393-8_38

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56393-8

  • Online ISBN: 978-3-540-47549-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation