Edinburgh Research Explorer

Constructing Induction Rules for Deductive Synthesis Proofs

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

Related Edinburgh Organisations

Open Access permissions

Open

Documents

http://dx.doi.org/10.1016/j.entcs.2005.08.003
Original languageEnglish
Title of host publicationElectronic Notes in Theoretical Computer Science
Subtitle of host publicationProceedings of the Workshop on the Constructive Logic for Automated Software Engineering (CLASE 2005)
Pages3–21
Volume153
DOIs
StatePublished - 2005

Publication series

NameElectronic Notes in Theoretical Computer Science
PublisherElsevier
ISSN (Print)1571-0661

Abstract

We describe novel computational techniques for constructing induction rules for deductive synthesis proofs. Deductive synthesis holds out the promise of automated construction of correct computer programs from specifications of their desired behaviour. Synthesis of programs with iteration or recursion requires inductive proof

    Research areas

  • deductive synthesis, proof planning, induction, theorem proving, middle-out reasoning

Download statistics

No data available

ID: 403407