Skip to main content
SpringerLink
Log in

On the connection between narrowing and proof by consistency

  • Conference paper
  • First Online:
Automated Deduction — CADE-12 (CADE 1994)

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

Included in the following conference series:

  • 150 Accesses

Abstract

We study the connection between narrowing and a method for proof by consistency due to Bachmair, and we show that narrowing and proof by consistency may be used to simulate each other. This allows for the migration of results between the two process descriptions. We obtain decidability results for validity of equations in the initial algebra from existing results on narrowing. Furthermore we show that several results on completeness of position selection strategies for narrowing are special cases of a generalization of a result on covering sets presented by Bachmair.

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. L. Bachmair. Proof by consistency in equational theories. In Proceedings 3rd IEEE Symposium on Logic in Computer Science, Edinburgh (UK), pages 228–233, 1988.

    Google Scholar 

  2. E. Bevers and J. Lewi. Proof by consistency in conditional equational theories. In Proceedings Second International Workshop on Conditional and Typed Rewriting Systems, volume 516 of Lecture Notes in Computer Science, pages 194–205. Springer-Verlag, 1990.

    Google Scholar 

  3. J. Chabin and P. Réty. Narrowing directed by a graph of terms. In Proceedings 4th Conference on Rewriting Techniques and Applications, Como (Italy), volume 488 of Lecture Notes in Computer Science, pages 112–123, 1991.

    Google Scholar 

  4. J. Christian. Some termination criteria for narrowing and E-narrowing. In Proceedings 11th International Conference on Automated Deduction, Saratoga Springs (NY, USA), volume 607 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1992.

    Google Scholar 

  5. R. Echahed. On completeness of narrowing strategies. Theoretical Computer Science, 72:133–146, 1990.

    Google Scholar 

  6. R. Echahed. Uniform narrowing strategies. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), volume 632 of Lecture Notes in Computer Science, pages 259–275. Springer-Verlag, 1992.

    Google Scholar 

  7. M. Fay. First-order unification in an equational theory. In Proceedings of the 4th Workshop on Automated Deduction, pages 161–167, 1979.

    Google Scholar 

  8. L. Fribourg. SLOG: A logic programming interpreter based on clausal superposition and rewriting. In Proceedings of the 1985 Symposium on Logic Programming, Boston, pages 172–184, 1985.

    Google Scholar 

  9. L. Fribourg. A strong restriction on the inductive completion procedure. In Proceedings 13th International Colloquium on Automata, Languages and Programming, volume 226 of Lecture Notes in Computer Science, pages 105–115. Springer-Verlag, 1986.

    Google Scholar 

  10. J. A. Goguen. How to prove inductive hypotheses without induction. In W. Bibel and R. Kowalski, editors, Proceedings of the 5th Conference on Automated Deduction, volume 87 of Lecture Notes in Computer Science, pages 356–373. Springer-Verlag, 1980.

    Google Scholar 

  11. G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, pages 239–266, 1982.

    Google Scholar 

  12. J.-M. Hullot. Canonical forms and unification. In Proceedings 5th International Conference on Automated Deduction, volume 87, pages 318–334. Springer-Verlag, 1980.

    Google Scholar 

  13. J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in theories without constructors. Information and Computation, 82(1):1–33, July 1989.

    Google Scholar 

  14. D. Kapur, P. Narendran, and H. Zhang. On sufficient-completeness and related properties of term rewriting systems. Acta Informatica, 24(4):395–415, 1987.

    Google Scholar 

  15. D. 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 

  16. W. Küchlin. Inductive completion by ground proof transformation. In H. AÏt-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 2 of Rewriting Techniques, chapter 7. Academic Press, 1989.

    Google Scholar 

  17. O. Lysne. Proof by consistency in constructive systems with final algebra semantics. In Proceedings 3rd International Conference on Algebraic and Logic Programming, Pisa (Italy), volume 632 of Lecture Notes in Computer Science, pages 276–290. Springer-Verlag, 1992.

    Google Scholar 

  18. J. Meseguer and J. A. Goguen. Initiality, induction and computability. In M. Nivat and J. C. Reynolds, editors, Algebraic Methods in Semantics, chapter 14. Cambridge University Press, 1985.

    Google Scholar 

  19. D. L. Musser. On proving inductive properties in abstract data types. In Proceedings of the 7th Annual ACM Symposium on Principles of Programming Languages, pages 154–162, January 1980.

    Google Scholar 

  20. W. Nutt, P. Réty, and G. Smolka. Basic narrowing revisited. Journal of Symbolic Computation, 7:295–317, 1989.

    Google Scholar 

  21. D. Plaisted. Semantic confluence tests and completion methods. Information and Control, 65:182–215, 1985.

    Google Scholar 

  22. P. Réty. Improving basic narrowing techniques. In Proceedings 2nd Conference on Rewriting Techniques and Applications, Bordeaux (France), volume 256 of Lecture Notes in Computer Science, pages 228–241. Springer-Verlag, 1987.

    Google Scholar 

  23. Jia-Huai You. Outer narrowing for equational theories based on constructors. In Proceedings 15th International Colloquium on Automata, Languages and Programming, Tampere (Finland), volume 317 of Lecture Notes in Computer Science, pages 727–741. Springer-Verlag, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Informatics, University of Oslo, Blindern, Po. box 1080, 0316, Oslo, Norway

    Olav Lysne

Authors
  1. Olav Lysne
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Alan Bundy

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lysne, O. (1994). On the connection between narrowing and proof by consistency. In: Bundy, A. (eds) Automated Deduction — CADE-12. CADE 1994. Lecture Notes in Computer Science, vol 814. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58156-1_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-58156-1_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-48467-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation