Abstract
How induction formulas are formulated in verification of Prolog programs is described. The same problem for well-founded induction was investigated by Boyer and Moore in their verification system for terminating LISP programs (BMTP). The least fixpoint semantics of Prolog provides us with the advantages that computational induction can be easily applied and can generate simpler induction schemes. We investigate how computational induction is applied to a class of first order formulas called S-formulas, in which specifications in our verification system are described. In addition, we show how equivalence preserving program transformation can be utilized to merge induction schemes into a simpler one when more than two induction schemes are suggested.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Apt, K.R. and M.H. van Emden, “Contribution to the Theory of Logic Programming”, J. ACM, Vol. 29, No. 3, pp. 841–862, 1982.
de Bakker, J.W. and D. Scott, “A Theory of Programs”, Unpublished Notes, IBM Seminar, Vienna, 1969.
Boyer,R.S. and J.S.Moore, “Computational Logic”, Chap.14–15, Academic Press, 1979.
Burstall, R., “Proving Properties of Programs by Structural Induction”, Comput.J., Vol. 12, No. 1, pp. 41–48, 1969.
Clark,K.L., “Predicate Logic as a Computational Formalism”, pp.75–76, Research Monograph: 79/59, TOC, Imperial College, 1979.
Clark,K.L. and S-Å.Tärnlund, “A First Order Theory of Data and Programs”, in Information Processing 77 (B.Gilchrist Ed), pp. 939–944, 1977.
van Emden, M.H. and R.A. Kowalski, “The Semantics of Predicate Logic as Programing Language”, J. ACM, Vol. 23, No. 4, pp. 733–742, 1976.
Gordon,M.J.,A.J.Milner and C.P.Wadsworth, “Edinburgh LCF — A Mechanized Logic of Computation' Lecture Notes in Computer Science 78, Springer, 1979.
Hagiya, M. and T. Sakurai, “Foundation of Logic Programming Based on Inductive Definition”, New Generation Computing, Vol.2, pp.59–77, 1984.
Jaffar, J.,J-L. Lassez and J. Lloyd, “Completeness of the Negation as Failure Rule”, Proc. 8th Internation: Joint Conference on Artificial Intelligence, Vol.1, pp.500–506, 1983.
Kanamori,T.and H.Seki, “Verification of Prolog Programs Using An Extension of Execution”, ICOT Technical Report, TR-093, 1984. Also Proc. 3rd International Conference on Logic Programming, 1986.
Kanamori, T.and K. Horiuchi, “Type Inference in Prolog and Its Applications”, ICOT Technical Report, TR-095, 1984. Also Proc. 9th International Joint Conference on Artificial Intelligence, Vol. 2, pp. 704–707, 1985.
Kowalski,R.A., “Logic for Problem Solving”, Chap. 10–12, North Holland,1980.
Murray, N.V., “Completely Non-Clausal Theorem Proving”, Artificial Intelligence, Vol. 18, pp. 67–85, 1982.
Pereira, L.M.,F.C.N. Pereira and D.H.D. Warren, “User's Guide to DECsystem-10 Prolog”, Occasional Paper 15, Dept. of Artificial Intelligence, Edinburgh, 1979.
Tamaki,H. and T.Sato, “Unfold/Fold Transformation of Logic Programs”, Proc. 2nd International Logic Programming Conference, pp. 127–138, 1984.
Tärnlund,S-Å., “Logic Programming Language Based on A Natural Deduction System”, UPMAIL Technical Report, No. 6, 1981.
Weyrauch,R.W. and R.Milner, “Program Correctness in A Mechanized Logic”, Proc. 1st USA-Japan Computer Conference, 1972.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1986 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kanamori, T., Fujita, H. (1986). Formulation of induction formulas in verification of prolog programs. In: Siekmann, J.H. (eds) 8th International Conference on Automated Deduction. CADE 1986. Lecture Notes in Computer Science, vol 230. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16780-3_97
Download citation
DOI: https://doi.org/10.1007/3-540-16780-3_97
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-16780-8
Online ISBN: 978-3-540-39861-5
eBook Packages: Springer Book Archive