Show simple item record

dc.contributor.authorKraan, Inaen
dc.date.accessioned2019-02-15T14:32:46Z
dc.date.available2019-02-15T14:32:46Z
dc.date.issued1994en
dc.identifier.urihttp://hdl.handle.net/1842/34920
dc.description.abstracten
dc.description.abstractThe area of logic program synthesis is attracting increased interest. Most efforts have concentrated on applying techniques from functional program synthesis to logic program synthesis. This thesis investigates a new approach: Synthesizing logic programs automatically via middle-out reasoning in proof planning.en
dc.description.abstract[Bundy et al 90a] suggested middle-out reasoning in proof planning. Middleout reasoning uses variables to represent unknown details of a proof. Unifica¬ tion instantiates the variables in the subsequent planning, while proof planning provides the necessary search control.en
dc.description.abstractMiddle-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.en
dc.description.abstractMiddle-out reasoning is also used to select induction schemes. Finding an appropriate induction scheme in synthesis is difficult, because the recursion in 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 applied to the 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.en
dc.description.abstractThe results reported in this thesis are encouraging. The approach has been implemented as an extension to the proof planner CUM [Bundy et al 90c], called Periwinkle, which has been used to synthesize a variety of programs fully automatically.en
dc.publisherThe University of Edinburghen
dc.relation.ispartofAnnexe Thesis Digitisation Project 2019 Block 22en
dc.relation.isreferencedbyen
dc.titleProof planning for logic program synthesisen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record