Skip to main content
SpringerLink
Log in

Rigid unification by completion and rigid paramodulation

  • Conference paper
  • First Online:
KI-94: Advances in Artificial Intelligence (KI 1994)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 861))

Included in the following conference series:

Abstract

This paper addresses the problem of computing complete sets of rigid-E-unifiers, initially introduced by Gallier, Narendran, Plaisted and Snyder who gave a proof of its NP-completeness. Our algorithm is based on completion and on a variant of basic paramodulation named rigid paramodulation. The crucial point of the algorithm is to ensure a constant orientation of the rules during the completion and the paramodulation process. This is achieved by defining minimal substitutions and proving that we can restrict our attention to such substitutions. This restriction allows us to use total term orderings because we don't need stability. We claim that our decision procedure becomes simpler. We prove soundness, completeness and termination of our algorithm.

Supported by a grant of the French-German PROCOPE-project.

Supported in part by a grant of the Alexander von Humboldt-Stiftung and the Alfried Krupp von Bohlen und Halbach-Stiftung.

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. P. Andrews. Theorem Proving via General Matings. J.ACM, 28(2):193–214, 1981.

    Google Scholar 

  2. G. Becher and U. Petermann. Rigid E-Unification by Completion and Rigid Paramodulation. Technical report, Cahiers du LAIAC (n. 22) Univ. of Caen, 1993.

    Google Scholar 

  3. B. Beckert. Ein vervollständigungsbasiertes Verfahren zur Behandlung von Gleichheit im Tableaukalkül mit freien Variablen. Master's thesis, Karlsruhe (TH), 1993.

    Google Scholar 

  4. W. Bibel. Automated Theorem Proving. Vieweg, 1st edition, 1982.

    Google Scholar 

  5. H. Comon. Solving inequations in term algebras. In C. S. P. IEEE, editor, Proceedings, LICS, Philadelphia, 1990.

    Google Scholar 

  6. N. Dershowitz. Termination of Rewriting. Journal of Symbolic Computation, 3(1&2):69–116, February/April 1987.

    Google Scholar 

  7. D. J. Dougherty and P. Johann. An Improved General E-Unification Method. Journal of Symbolic Computation, 14:303–320, 1992.

    Google Scholar 

  8. J. Gallier, P. Narendran, D. Plaisted, S. Raatz, and W. Snyder. An Algorithm for finding Canonical Sets of Ground Rewrite Rules in Polynomial Time. Journal of the A.C.M., 40:1–16, January 1993.

    Google Scholar 

  9. J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Rigid E-unification: NP-Completeness and Applications to Equational Matings. Information and Computation, pages 129–195, 1990.

    Google Scholar 

  10. J. Gallier and W. Snyder. Complete Sets of Transformations for General E-Unification. Theoretical Computer Science, 67:203–260, 1989.

    Google Scholar 

  11. J. Goubault. A Rule-Based Algorithm for Rigid E-Unification. In 3rd Kurt Gödel Colloquium '93, volume 713 of LNCS. Springer-Verlag, 1993.

    Google Scholar 

  12. J.-M. Hullot. Canonical Forms and Unification. In Proceedings CADE, pages 318–334. Springer-Verlag, 1980. Lecture Notes in Artificial Intelligence 87.

    Google Scholar 

  13. J.-P. Jouannaud and C. Kirchner. Solving Equations in Abstract Algebras: A Rule-based Survey of Unification. Computational Logic. Essays in Honour of Alan Robinson, pages 257–321, 1991.

    Google Scholar 

  14. D. Kozen. Positive first-order logic is NP-complete. IBM Journal of Research and Development, 4:327–332, 1981.

    Google Scholar 

  15. J. Kruskal. Well Quasi Ordering, the Tree Problem and Vazsonyi's conjecture. Transactions of the American Mathematical Society, 95:210–225, 1960.

    Google Scholar 

  16. D. W. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1978.

    Google Scholar 

  17. G. Nelson and D. C. Oppen. Fast Decision Procedures Based on Congruence Closure. Journal of Association for Computer Machinery, 27(2), April 1980.

    Google Scholar 

  18. D. A. Plaisted. A simple non-termination test for the Knuth-Bendix method. In Proc 8th CADE, LNCS 230, pages 79–88. Springer, 1986.

    Google Scholar 

  19. D. A. Plaisted. Polynomial Time Termination and Constraint Satisfaction Tests. In Rewriting Techniques and Applications, pages 405–420, Montreal, June 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LAIAC Université de Caen, 14032, Caen Cedex, France

    Gérard Becher

  2. FB IMN, HTWK Leipzig, Postfach 66, D-04251, Leipzig, FRG

    Uwe Petermann

Authors
  1. Gérard Becher
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Uwe Petermann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Bernhard Nebel Leonie Dreschler-Fischer

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Becher, G., Petermann, U. (1994). Rigid unification by completion and rigid paramodulation. In: Nebel, B., Dreschler-Fischer, L. (eds) KI-94: Advances in Artificial Intelligence. KI 1994. Lecture Notes in Computer Science, vol 861. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58467-6_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-58467-6_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58467-4

  • Online ISBN: 978-3-540-48979-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation