Middle-Out Reasoning for Logic Program Synthesis

I. Kraan, D. Basin, Alan Bundy

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 verication proof. The approach is a two-level one: At the object level, we prove program verication conjectures in a sorted, rst-order theory. The conjectures are of the form 8args ! : prog(args ! ) $ spec(args ! ). At the meta-level, we plan the object-level verication with an unspecied program denition. The denition is represented with a (second-order) meta-level variable, which becomes instantiated in the course of the planning.
Original languageEnglish
Title of host publicationProceedings of the Tenth International Conference on Logic Programming
PublisherMIT Press
Number of pages12
ISBN (Print) 9780262731058
Publication statusPublished - 1993
EventProceedings of the Tenth International Conference on Logic Programming June 21-24, 1993 - Budapest, Hungary
Duration: 21 Jun 199324 Jun 1993

Conference

ConferenceProceedings of the Tenth International Conference on Logic Programming June 21-24, 1993
CountryHungary
CityBudapest
Period21/06/9324/06/93

Keywords

  • logic program synthesis
  • proof planning
  • Automated theorem proving

Fingerprint Dive into the research topics of 'Middle-Out Reasoning for Logic Program Synthesis'. Together they form a unique fingerprint.

Cite this