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
StatePublished - 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