Skip to main content
SpringerLink
Log in
Book cover

International Conference on Rewriting Techniques and Applications

RTA 1989: Rewriting Techniques and Applications pp 76–91Cite as

Inductive proofs by specification transformations

  • Regular Papers
  • Conference paper
  • First Online:

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

Abstract

We show how to transform equational specifications with relations between constructors (or without constructors) into order-sorted equational specifications where every function symbol is either a free constructor or a completely defined function.

This method allows to reduce the problem of inductive proofs in equational theories to Huet and Hullot's proofs by consistency [HH82]. In particular, it is no longer necessary to use the socalled “inductive reducibility test” which is the most expensive part of the Jouannaud and Kounalis algorithm [JK86].

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

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 Proc. 3rd IEEE Symp. Logic in Computer Science, Edinburgh, July 1988.

    Google Scholar 

  2. H. Comon and P. Lescanne. Equational Problems and Disunification. Research Report Lifia 82 Imag 727, Univ. Grenoble, May 1988. To appear in J. Symbolic Computation.

    Google Scholar 

  3. H. Comon. An effective method for handling initial algebras. In Proc. 1st Workshop on Algebraic and Logic Programming, Gaussig, 1988.

    Google Scholar 

  4. H. Comon. Unification et Disunification: Théorie et Applications. Thèse de Doctorat, I.N.P. de Grenoble, France, 1988.

    Google Scholar 

  5. H. Comon and J.-L. Remy. How to Characterize the Language of Ground Normal Forms. Research Report 676, INRIA, June 1987.

    Google Scholar 

  6. L. Fribourg. A strong restriction of the inductive completion procedure. In Proc. 13th ICALP, Rennes, LNCS 226, pages 105–115, Springer-Verlag, 1986.

    Google Scholar 

  7. J. H. Gallier and R. V. Book. Reductions in tree replacement systems. Theoretical Computer Science, 37:123–150, 1985.

    Google Scholar 

  8. J. Goguen and J. Meseguer. Order-Sorted Algebra I: Partial and Overloaded Operators, Errors and Inheritance. Draft, Computer Science Lab., SRI International, 1987.

    Google Scholar 

  9. J. A. Goguen. How to prove inductive hypothesis without induction. In Proc. 5th Conf. on Automated Deduction, LNCS 87, 1980.

    Google Scholar 

  10. G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2), 1982.

    Google Scholar 

  11. J.-P. Jouannaud and E. Kounalis. Automatic proofs by induction in equational theories without constructors. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., June 1986.

    Google Scholar 

  12. C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of obj-3. In Proc. 15th Int. Conf on Automata, Languages and Programming, LNCS 317, Springer-Verlag, July 1988.

    Google Scholar 

  13. D. Kapur and R. D. Musser. Inductive reasoning with incomplete specifications. In Proc. 1st IEEE Symp. Logic in Computer Science, Cambridge, Mass., June 1986.

    Google Scholar 

  14. D. Kapur and D. Musser. Proof by consistency. Artificial Intelligence, 31(2), February 1987.

    Google Scholar 

  15. D. Kapur, P. Narendran, and H. Zhang. On Sufficient Completeness and Related Properties of Term Rewriting Systems. Research Report, General Electric Company, October 1985. Preprint.

    Google Scholar 

  16. D. Kapur, P. Narendran, and H. Zhang. Proof by induction using test sets. In Proc. 8th Conf. on Automated Deduction, Oxford, LNCS 230, Springer-Verlag, July 1986.

    Google Scholar 

  17. W. Kuchlin. Inductive Completion by Ground Proofs Transformation. Research Report, University of Delaware, February 1987.

    Google Scholar 

  18. D. Lankford. A simple explanation of inductionless induction. Technical Report MTP-14, Mathematics Department, Louisiana Tech. Univ., 1981.

    Google Scholar 

  19. D. Musser. Proving inductive properties of abstract data types. In Proc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, 1980.

    Google Scholar 

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

    Google Scholar 

  21. G. Smolka, W. Nutt, J. Goguen, and J. Meseguer. Order-Sorted Equational Computation. SEKI Report SR-87-14, Univ. Kaiserslautern, December 1987.

    Google Scholar 

  22. S. R. Thatte. On the correspondance between two classes of reductions systems. Information Processing Letters, 20:83–85, February 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d'Informatique fondamentale et d'Intelligence Artificielle, Institut IMAG, 46 Ave. Félix Viallet, 38031, Grenoble cedex, France

    Hubert Comon

Authors
  1. Hubert Comon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Nachum Dershowitz

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Comon, H. (1989). Inductive proofs by specification transformations. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_101

Download citation

  • DOI: https://doi.org/10.1007/3-540-51081-8_101

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-51081-9

  • Online ISBN: 978-3-540-46149-4

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation