TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 9530

Automation of Proof by Mathematical Induction

( Jul 24 – Jul 28, 1995 )

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/9530

Organizers
  • A. Bundy
  • Ch. Walther
  • D. Kapur
  • R.S. Boyer



Motivation

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.

Copyright

Participants
  • A. Bundy
  • Ch. Walther
  • D. Kapur
  • R.S. Boyer