Constructing Induction Rules for Deductive Synthesis Proofs
Electronic Notes in Theoretical Computer SciencePublished 1 March 2006Open access
Alan Bundy, Lucas Dixon, Jeremy Gow, Jacques Fleuriot
Citations2,811
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
It is shown that a combination of rippling and the use of meta-variables as a least-commitment device can provide novelty in induction rule construction techniques that can introduce novel recursive structures.
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
Keywords
Computer Science
The Journal of Logic ProgrammingThe integration of functions into logic programming: From theory to practice
426 Citations1994Michael Hanus
The development of the operational semantics as well as the improvement of the implementation of the implementation of functional logic languages are surveyed.
Lecture notes in computer scienceIsaPlanner: A Prototype Proof Planner in Isabelle
202 Citations2003Lucas Dixon, Jacques Fleuriot
The approach to proof planning is introduced, an overview of IsaPlanner is given, and one simple yet effective reasoning technique is presented.
Journal of Automated ReasoningProductive use of failure in inductive proof
164 Citations1996Andrew Ireland, Alan Bundy
It is shown how the failure if rippling can be used in bridging gaps in the search for inductive proofs, and a novel theorem-proving architecture for supporting the automatic discovery of eureka steps is presented.
Cambridge University Press eBooksRippling: Meta-Level Guidance for Mathematical Reasoning
141 Citations2005Alan Bundy, David Basin +2 more
This book presents a meta-analysis of rippling using an annotated calculus and a unification algorithm as a guide to a general methodology for efficient use of failure.
Acta InformaticaA synthesis of several sorting algorithms
131 Citations1978John Darlington
This work synthesises versions of six well known sorting algorithms from a common specification using program transformation techniques, building up a family tree for the sorts exposing certain relationships between them.
Artificial IntelligenceOn proving the termination of algorithms by machine
69 Citations1994Christoph Walther
This work shows how a termination hypothesis for an algorithm is synthesized by machine, which knowledge about algorithms is required for an automated synthesis, and how this knowledge is computed.
Journal of Automated ReasoningMiddle-out reasoning for synthesis and induction
37 Citations1996Ina Kraan, David Basin +1 more
Two applications of middle-out reasoning in inductive proofs are developed: logic program synthesis and the selection of induction schemes, and a variaety of programs is synthesized fully automatically.
Lecture notes in computer science10th International Conference on Automated Deduction
20 Citations1990International Conference on Automated Deduction 1990 Kaiserslautern, Stickel, Mark E.
TUbilio (Technical University of Darmstadt)Combining induction axioms by machine
19 Citations1993Christoph Walther
A commutation test is developed as a deductive requirement to verify the soundness of the combined axiom, and it is shown how so-called commutation formulas can be derived by machine from the given axioms such that a verification of these formulas guarantees the well-foundcdness ofThe usefulness and strength of the proposed technique.
Lecture notes in computer scienceSynthesis of induction orderings for existence proofs
16 Citations1994Dieter Hutter
A top-down approach for computing appropriate induction orderings for existence formulas by using constraints from the knowledge of guiding inductive proofs to select proper induction variables and to compute a first outline of the proof.
Edinburgh Research Archive (University of Edinburgh)The Dynamic Creation of Induction Rules Using Proof Planning
15 Citations2004Jeremy Gow
A new delayed commitment strategy for inductive proof that generates a wider range of useful induction rules than other delayed commitment techniques, partly because it removes unnecessary restrictions on the individual proof cases, and partly because of a new technique for generating the rule’s overall case structure.
Edinburgh Research Archive (University of Edinburgh)Proof planning for logic program synthesis
12 Citations1994Ina Kraan
Lecture notes in computer scienceExtensions to the Estimation Calculus
4 Citations1999Jeremy Gow, Alan Bundy +1 more