BRICS · Contents · Programme · Lecture Notes

Induction Based on Rippling and Proof Planning

A BRICS Mini-Course
August 11, 1994

Lectures by
David Basin
Max-Planck-Institut für Informatik, Saarbrücken, Germany


Course Contents

Mathematical Induction is a central technique in reasoning about programs and their properties, e.g., loops and recursion, recursively defined data-structures, and program termination. For researchers interested in establishing these properties on a computer, such reasoning must be automated or at least partially supported. In this five hour seminar some of the central issues in automating proof by mathematical induction will be covered. In particular, formalisms for mathematical induction, techniques for selecting induction schemata and well-founded orders, rewriting in inductive theorem proving, and applications. The topics will often be illustrated using ideas and techniques that have been developed at Edinburgh and embodied in the CLAM Inductive Theorem Proving System.

Programme

Thursday August 11, 1994, 09:30-10:30

Introduction
  • Why inductive theorem proving is hard
  • Motivate finding proofs invariants (leading up to use of Ind. Hyp.)
  • Motivate Rippling
    • general idea: structure invariant terminating rewriting
    • Edinburgh (Clam perspective)
    • INKA perspective
  • Overview of "induction architectures" based on rippling (e.g., Clam & Inka)

Thursday August 11, 1994, 10:45-11:45

Theory/Alternatives
  • Termination of rippling
  • Incorporating new (domain dependent) termination orderings
  • Rippling Calculi (as in Clam and INKA)

Thursday August 11, 1994, 13:00-14:00

Extensions/applications of rippling
  • Colors as a solution to problem of multiple induction hypotheses
  • Program Synthesis (e.g., existential quantifiers & metavariables)
  • NonInductive Problems
    • equational reasoning (e.g., Lim+, symbolic algebra)

Thursday August 11, 1994, 14:15-15:15

Planning and Critics
  • advantages of proof plans as explicit objects
  • critics for failure analysis
    • missing lemmas, generalizations, ...

Thursday August 11, 1994, 15:45-16:45

Misc
  • Induction Schema selection/significance of underlying logic/...
  • Relationship to other approaches (NQTHM, Inductive Completion, ...)

Lecture Notes

BRICS-NS-94-2