## 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 ∀−→−−args.prog(−→−−args)↔spec(−→−−args). . 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.

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.

Original language | English |
---|---|

Title of host publication | Logic Program Synthesis and Transformation |

Subtitle of host publication | Proceedings of LOPSTR 92, International Workshop on Logic Program Synthesis and Transformation, University of Manchester, 2-3 July 1992 |

Publisher | Springer London |

Pages | 1-14 |

ISBN (Electronic) | 978-1-4471-3560-9 |

ISBN (Print) | 978-3-540-19806-2 |

DOIs | |

Publication status | Published - 1993 |

### Publication series

Name | Workshops in Computing |
---|---|

Publisher | Springer London |

ISSN (Print) | 1431-1682 |