Middle-out reasoning for synthesis and induction

Ina Kraan, David Basin, Alan Bundy

Research output: Contribution to journalArticlepeer-review


We develop two applications of middle-out reasoning in inductive proofs: logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first suggested by Bundy et al. Middle-out reasoning uses variables to represent unknown terms and formulae. Unification instantiates the variables in the subsequent planning, while proof planning provides the necessary search control.

Middle-out reasoning is used for synthesis by planning the verification of an unknown logic program: The program body is represented with a meta-variable. The planning results both in an instantiation of the program body and a plan for the verification of that program. If the plan executes successfully, the synthesized program is partially correct and complete.

Middle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme during synthesis is difficult because the recursion of the program, which is unknown at the outset, determines the induction in the proof. In middle-out induction, we set up a schematic step case by representing the constructors that are applied to induction variables with meta-variables. Once the step case is complete, the instantiated variables correspond to an induction appropriate to the recursion of the program.

We have implemented these techniques as an extension of the proof planning system CLAM, called Periwinkle, and synthesized a variety of programs fully automatically.

Original languageEnglish
Pages (from-to)113-145
Number of pages33
JournalJournal of Automated Reasoning
Issue number1-2
Publication statusPublished - 1996


  • logic program synthesis
  • metavariables
  • induction
  • proof planning
  • Automated theorem proving
  • higher-order unification


Dive into the research topics of 'Middle-out reasoning for synthesis and induction'. Together they form a unique fingerprint.

Cite this