The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

MSc Thesis #94128

Title:Generator Induction for Relational Proofs, Logic Program Synthesis and Reasoning About Database Systems
Date: 1994
Abstract:There are many potential uses for an induction scheme that can handle relational definitions of datatypes, and also work in a dynamic fashion with many different datatypes. For example, one interesting use would be to reason about interrelationships between recursive queries to deductive databases. One could also hope to synthesise appropriate queries given some specification written in terms of existing queries. We present one such scheme which we call generator induction (GI). This rule is written in terms of a predicate and its definition (which will be the completion of a set of Horn clauses for this "induction predicate"). We demonstrate that GI is consistent with logic program synthesis by implementing it in the whelk system. We show that we can recover the standard structural inductions from GI, and then present a selection of both verification and synthesis proofs using the GI with relationally defined induction predicates. The use of the GI rule itself is usually straightforward with few choices. However, after the GI phase is complete we are left with a situation in which the variables in the induction hypotheses, and the conclusion are linked by relations, instead of the equalities that were the norm for structural inductions. thus, the completion of the proof after this GI phase will usually be much more difficult. We briefly analyse the proofs, and see indications that rippling ideas are applicable.

[Search These Pages] [DAI Home Page] [Comment]