Abstract
We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At the object level, we prove program verification conjectures in a sorted, first-order theory. The conjectures are of the form\( \forall \xrightarrow[{\arg s.}]{}prog(\xrightarrow[{\arg s}]{}) \leftrightarrow spec(\xrightarrow[{\arg s}]{}). \) . At the meta-level, we plan the object-level verification with an unspecified program definition. The definition is represented with a (second-order) meta-level variable, which becomes instantiated in the course of the planning.
This technique is an application of the Clam proof planning system [Bundy et al 90c]. Clam is currently powerful enough to plan verification proofs for given programs. We show that, if Clam’s use of middle-out reasoning is extended, it will also be able to synthesize programs.
Supported by the German Ministry for Research and Technology (BMFT) under grant ITS 9102. Responsibility for the contents of this publication lies with the authors.
Supported by SERC grant GR/E/44598, Esprit BRA grant 3012, Esprit BRA grant 3245, and an SERC Senior Fellowship.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Joseph L. Bates and Robert L. Constable. Proofs as programs. ACM Transactions on Programming Languages and Systems, 7 (1): 113–136, January 1985.
W. Bibel. Syntax-directed, semantics-supported program synthesis. Artificial Intelligence, 14: 243–261, 1980.
S. Biundo. Automated synthesis of recursive algo rithms as a theorem proving tool. In Y. Kodratoff, editor, Eighth European Conference on Artificial Intelligence, pages 553–8. Pitman, 1988.
R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988. Perspectives in Computing, Vol 23.
A. Bundy. The use of explicit plans to guide inductive proofs. In R. Lusk and R. Overbeek, editors, 9th Conference on.Automated Deduction, pages 111–120. Springer-Verlag, 1988. Longer version available from Edinburgh as DAI Research Paper No. 349.
A. Bundy, F. van Harmelen, J. Hesketh, A. Smaill, and A. Stevens. A rational reconstruction and extension of recursion analysis. In N.S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, pages 359–365. Morgan Kauf-mann, 1989. Also available from Edinburgh as DAI Research Paper 419.
Bundy et al 90a] A. Bundy, A. Smaill, and J. Hesketh. Turning eureka steps into calculations in automatic program synthesis. In S.L.H. Clarke, editor,Proceedings of UK IT 90,pages 221–6, 1990. Also available from Edinburgh as DAI Research Paper 448.
A. Bundy, A. Smaill, and G. A. Wiggins. The synthesis of logic programs from inductive proofs. In J. Lloyd, editor, Computational Logic) pages 135–149. Springer- Verlag, 1990. Esprit Basic Research Series. Also available from Edinburgh as DAI Research Paper 501.
A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.
R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.
Y. Deville. Logic Programming. Systematic Program Development. International Series in Logic Programming. Addision-Wesley, 1990.
L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In Proceedings of Eighth International Conference on Logic Programming, pages 685–699. MIT Press, June 1990.
P. Hill and J. Lloyd. The Godei Report. Technical Report TR-91–02, Department of Computer Science,University of Bristol, March 1991. Revised in September 1991.
C.J. Hogger. Derivation of logic programs. J ACM, 28 (2): 372–392, April 1981.
W.A. Howard. The formulae-as-types notion of construction. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry; Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479–490. Academic Press, 1980.
Per Martin-Lof. Constructive mathematics and computer programming. In 6th International Congress for Logic, Methodology and Philosophy of Science, pages 153–175, Hanover, August 1979. Published by North Holland, Amsterdam. 1982.
Wiggins 92]
G. A. Wiggins. Synthesis and transformation of logic programs in the Whelk proof development system. In K. R. Apt, editor, Proceedings of JICSLP-92, 1992.
G. A. Wiggins, A. Bundy, H. C. Kraan, and J. Hes-keth. Synthesis and transformation of logic programs through constructive, inductive proof. In K-K. Lau and T. Clement, editors, Proceedings of LoPSTr-91, pages 27–45. Springer Verlag, 1991. Workshops in Computing Series.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Springer-Verlag London
About this chapter
Cite this chapter
Kraan, I., Basin, D., Bundy, A. (1993). Logic Program Synthesis via Proof Planning. In: Lau, KK., Clement, T.P. (eds) Logic Program Synthesis and Transformation. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3560-9_1
Download citation
DOI: https://doi.org/10.1007/978-1-4471-3560-9_1
Publisher Name: Springer, London
Print ISBN: 978-3-540-19806-2
Online ISBN: 978-1-4471-3560-9
eBook Packages: Springer Book Archive