Skip to main content
SpringerLink
Log in

Sufficient completeness and parameterized proofs by induction

  • Conference paper
  • First Online:
Algebraic and Logic Programming (ALP 1994)

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

Included in the following conference series:

  • 133 Accesses

Abstract

Theorem proving in parameterized specifications allows for shorter and more structured proofs. Moreover, a generic proof can be given just once and reused for each instantiation of the parameters. We present procedures to test sufficient completeness and to prove and disprove inductive properties automatically in parameterized conditional specifications. This new method when limited to non-parameterized conditional specifications, can refute general clauses; refutational completeness is also preserved for boolean ground convergent rewrite systems even if the functions are not sufficiently complete and the constructors are not free. The method has been implemented in the prover SPIKE. Based on computer experiments, the method appears to be more practical and efficient than inductive theorem proving in non-parameterized specifications. Moreover, SPIKE offers facilities to check and complete definitions.

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, Cambridge (Mass., USA), pages 228–233, 1988.

    Google Scholar 

  2. K. Becker. Inductive Proofs in Specifications Parameterized by a Built-in Theory. SEKI-Report, SR-92-02, 1992.

    Google Scholar 

  3. A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Technical Report 1636, INRIA, 1992.

    Google Scholar 

  4. A. Bouhoula and M. Rusinowitch. Automatic Case Analysis in Proof by Induction. In Proceedings of the 13th International Joint Conference on Artificial Intelligence, volume 1, page 88–94. Chambéry France, 1993.

    Google Scholar 

  5. A. Bouhoula and M. Rusinowitch. Implicit Induction in Conditional Theories. Journal of Automated Reasoning, accepted in June 1994. To appear.

    Google Scholar 

  6. A. Bouhoula. Parameterized Specifications: Sufficient Completeness and Implicit Induction. Technical Report 2129, INRIA, 1993.

    Google Scholar 

  7. A. Bouhoula. Preuves Automatiques par Récurrence dans les Théories Conditionnelles. PhD thesis, Université de Nancy I, Mars 1994.

    Google Scholar 

  8. A. Bouhoula. Spike: a system for sufficient completeness and parameterized inductive proof. In Proceedings 12th International Conference on Automated Deduction, Nancy (France), Lecture Notes in Artificial Intelligence. Springer-Verlag, June 1994. To appear.

    Google Scholar 

  9. R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979.

    Google Scholar 

  10. H. Comon. Sufficient Completeness, Term rewriting Systems and “Anti-Unification”. In Proceedings 8th International Conference on Automated Deduction, Oxford, England, July 1986.

    Google Scholar 

  11. N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69–116, 1987.

    Google Scholar 

  12. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leuven, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers North-Holland, 1990.

    Google Scholar 

  13. H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. Springer Verlag, 1985.

    Google Scholar 

  14. H. Ganzinger. Ground Term Confluence in Parametric Conditional Rewrite Systems. In STACS'87, volume 247 of LNCS, pages 286–298. Springer-Verlag, 1987.

    Google Scholar 

  15. J. V. Guttag and J. J. Horning The Algebraic Specification of Abstract Data Types. In Acta Informatica, 10:27–52, 1978.

    Google Scholar 

  16. G. Huet and J.-M. Hullot. Proofs by induction in equational theories with constructors. Journal of Computer and System Sciences, 25(2):239–266, October 1982.

    Google Scholar 

  17. J.-P. Jouannaud and E. Kounalis. Proof by induction in equational theories without constructors. In Proceedings 1st IEEE Symposium on Logic in Computer Science, Cambridge (Mass., USA), pages 358–366, 1986.

    Google Scholar 

  18. H. Kirchner. Proofs in Parameterized Specifications. In 4th RTA, volume 488 of LNCS, pages 174–187. Springer-Verlag, 1991.

    Google Scholar 

  19. E. Kounalis. Completeness in Data Type Specifications. In Proceeding EUROCAL Conference. Springer-Verlag, Linz (Austria), 1991.

    Google Scholar 

  20. E. Kounalis and M. Rusinowitch. Mechanizing inductive reasoning. In Proceedings of the American Association for Artificial Intelligence Conference, Boston, pages 240–245. AAAI Press and MIT Press, July 1990.

    Google Scholar 

  21. A. Lazrek, P. Lescanne, and J.-J. Thiel. Tools for proving inductive equalities, relative completeness and ω-completeness. Information and Computation, 84(1):47–70, January 1990.

    Google Scholar 

  22. D. R. Musser. On proving inductive properties of abstract data types. In Proceedings 7th ACM Symp. on Principles of Programming Languages, pages 154–162. Association for Computing Machinery, 1980.

    Google Scholar 

  23. M. Navarro and F. Orejas. Parameterized Horn clause specifications: proof theory and correctness. In Proceeding TAPSOFT Conference, volume 249 of LNCS. pages 202–216, Springer-Verlag, 1987.

    Google Scholar 

  24. P. Padawitz. Towards a proof theory of parameterized specifications. In Semantics of data type's, volume 173 of LNCS, pages 375–391. Springer-Verlag, 1984.

    Google Scholar 

  25. P. Padawitz. Parameter-Preserving Data Type Specifications. In Journal of Computer and System Science, volume 34, pages 179–209, 1987.

    Google Scholar 

  26. U. S. Reddy. Term rewriting induction. In M. E. Stickel, editor, Proceedings 10th ICADE, Kaiserslautern (Germany), volume 449 of LNCS, pages 162–177. Springer-Verlag, 1990.

    Google Scholar 

  27. M. Wirsing. Algebraic specification. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science B: Formal Methods and Semantics, chapter 13, pages 675–788. Elsevier, Amsterdam, 1990.

    Google Scholar 

  28. H. Zhang, D. Kapur, and M. S. Krishnamoorthy. A mechanizable induction principle for equational specifications. In Proceedings 9th ICADE, Argonne (Ill., USA), volume 310 of LNCS, pages 162–181. Springer-Verlag, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CRIN & INRIA-Lorraine, BP 239, 54506, Vandœuvre-lès-Nancy, France

    Adel Bouhoula

Authors
  1. Adel Bouhoula
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Giorgio Levi Mario Rodríguez-Artalejo

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag

About this paper

Cite this paper

Bouhoula, A. (1994). Sufficient completeness and parameterized proofs by induction. In: Levi, G., Rodríguez-Artalejo, M. (eds) Algebraic and Logic Programming. ALP 1994. Lecture Notes in Computer Science, vol 850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58431-5_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-58431-5_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58431-5

  • Online ISBN: 978-3-540-48791-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation