Constructing Induction Rules for Deductive Synthesis Proofs

Alan Bundy, Lucas Dixon, Jeremy Gow, Jacques Fleuriot

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

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
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
Publication statusPublished - 2005

Publication series

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

Keywords

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

Fingerprint

Dive into the research topics of 'Constructing Induction Rules for Deductive Synthesis Proofs'. Together they form a unique fingerprint.

Cite this