Mathematical induction is required for reasoning about objects or events containing repetition, e.g. computer programs with recursion or iteration, electronic circuits with feedback loops or parameterized components. Thus mathematical induction is a key enabling technology for the use of formal methods in information technology. Failure to automate inductive reasoning is one of the major obstacles to the widespread use of formal methods in industrial hardware and software development.

Recent developments in automatic theorem proving promise significant improvements in our ability to automate mathematical induction. As a result of these developments, the functionality of inductive theorem provers has begun to improve. Moreover, there are some promising signs that even more significant improvements are possible. This enlarges the applicability of automated induction for “real world” problems and research topics for application have been discussed on the seminar.

Automated induction is a relatively small subfield of automated reasoning. Research is based on two competing paradigms each having its merits but also its shortcomings as compared with the other:

• Implicit induction evolved from Knuth-Bendix-Completion and most of the work based on this paradigm was performed by researchers concerned with term rewriting systems in general.
• Explicit induction has its roots in traditional automated theorem proving. It resembles the more familiar idea of theorem proving by induction where induction axioms are explicitly given and specific inference techniques are tailored for proving base and step formulas.

This seminar brought together leading scientists from both areas to discuss recent advancements within both paradigms, to evaluate and compare the state of the art and to work for a synthesis of both approaches. It summarized the results of a series of workshops held on automated induction in conjunction with the CADE conferences 1992 (Saratoga Springs) and 1994 (Nancy) and the AAAI conference 1993 (Washington DC).

The success of this meeting was due in no small part to the Dagstuhl Seminar Center and its staff for creating such a friendly and productive environment. The organizers and participants greatly appreciate their effort. The organizers also thank J¨urgen Giesl and Martin Protzen for their support in many organizational details.

Creative Commons BY 3.0 DE