Automation of Proofs by Mathematical Induction


Keywords: mathematical induction

Start Date: 1 January 93 / Status: finished / Duration: 24 months

[ participants / contact]

Objectivies and Approach

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 parameterised components. It is thus a vital ingredient of formal methods techniques for synthesiting, verifying and transforming software and hardware. The automation of induction proof will improve the capability of mechanical assistants for software and hardware designers. It will reduce the need for such designers to be skilled in mathematical proof techniques and will improve their productivity by automating tedious and error-prone aspects of their task.

The aim of this cooperative activity is to encourage cross-fertilisation amongst researchers in the area of automation of mathematical proofs requiring induction. It takes the form of joint workshops and bilateral visits, which will encourage the cross-fertilisation of complementary skills and approaches and stimulate significant advances.

European links: European partners are also involved in related ESPRIT projects COMPULOG 2 (6810), COMPULOG NET (7230) and TYPES (6453).


University of Edingburgh
Artificial Intelligence
South Bridge, 80

EU Partners

University of Edingburgh, UK
Darmstadt University, D
Max-Planck-Institut, Saarbrücken, D
Tübingen University, D
Universität Kaiserslautern, D
DFKI GmbH, Saarbrücken, D
University Paris-Sud, F
University of Cambridge, UK
Oxford University, UK

Non-EU Partners

University of Illinois at Champaign, USA
University of Texas at Austin, USA
University of Iowa, USA
Ohio State University, USA


Prof. Alan Bundy
Phone: +44 31 650 2716
Fax: +44 31 650 6516

INCO synopses home page INCO cooperation index INCO keyword index
INCO acronym index INCO number index INCO Working Groups index
synopses home page all keywords index all acronyms index all numbers index

MIND/INDUS - EC-US019, May 1997

please address enquiries to the ESPRIT Information Desk

html version of synopsis by Nick Cook