Automation of Proofs by Mathematical Induction


MIND/INDUS - EC-US019

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).


Coordinator

University of Edingburgh
Artificial Intelligence
South Bridge, 80
EDINBURGH EH1 1HN, UK

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
CRIN-INRIA, F
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

CONTACT POINT

Prof. Alan Bundy
Phone: +44 31 650 2716
Fax: +44 31 650 6516
E-mail: bundy@edinburgh.ac.uk


INCO synopses home page INCO cooperation index INCO keyword index
INCO acronym index INCO number index INCO Working Groups index
All
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