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.
Keywords
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
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.
K. Becker. Inductive Proofs in Specifications Parameterized by a Built-in Theory. SEKI-Report, SR-92-02, 1992.
A. Bouhoula, E. Kounalis, and M. Rusinowitch. Automated mathematical induction. Technical Report 1636, INRIA, 1992.
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.
A. Bouhoula and M. Rusinowitch. Implicit Induction in Conditional Theories. Journal of Automated Reasoning, accepted in June 1994. To appear.
A. Bouhoula. Parameterized Specifications: Sufficient Completeness and Implicit Induction. Technical Report 2129, INRIA, 1993.
A. Bouhoula. Preuves Automatiques par Récurrence dans les Théories Conditionnelles. PhD thesis, Université de Nancy I, Mars 1994.
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.
R. S. Boyer and J. S. Moore. A Computational Logic. Academic Press, New York, 1979.
H. Comon. Sufficient Completeness, Term rewriting Systems and “Anti-Unification”. In Proceedings 8th International Conference on Automated Deduction, Oxford, England, July 1986.
N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1 & 2):69–116, 1987.
N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leuven, editor, Handbook of Theoretical Computer Science. Elsevier Science Publishers North-Holland, 1990.
H. Ehrig, B. Mahr. Fundamentals of Algebraic Specification 1. Equations and Initial Semantics. Springer Verlag, 1985.
H. Ganzinger. Ground Term Confluence in Parametric Conditional Rewrite Systems. In STACS'87, volume 247 of LNCS, pages 286–298. Springer-Verlag, 1987.
J. V. Guttag and J. J. Horning The Algebraic Specification of Abstract Data Types. In Acta Informatica, 10:27–52, 1978.
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.
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.
H. Kirchner. Proofs in Parameterized Specifications. In 4th RTA, volume 488 of LNCS, pages 174–187. Springer-Verlag, 1991.
E. Kounalis. Completeness in Data Type Specifications. In Proceeding EUROCAL Conference. Springer-Verlag, Linz (Austria), 1991.
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.
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.
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.
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.
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.
P. Padawitz. Parameter-Preserving Data Type Specifications. In Journal of Computer and System Science, volume 34, pages 179–209, 1987.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Rights 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