July 24 – 28 , 1995, Dagstuhl Seminar 9530

Automation of Proof by Mathematical Induction


R.S. Boyer, A. Bundy, D. Kapur, Ch. Walther

For support, please contact

Dagstuhl Service Team


Dagstuhl-Seminar-Report 122


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.


In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.