Edinburgh Research Explorer

Middle-Out Reasoning for Logic Program Synthesis

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

Related Edinburgh Organisations

Documents

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

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.

    Research areas

  • logic program synthesis, proof planning, Automated theorem proving

Event

ID: 25316721