BUNDY

Logic and Computation
AUTOMATING INDUCTIVE PROOFS

Advanced course

ALAN BUNDY

Department of Artificial Intelligence, University of Edinburgh

First week
A.Bundy@ed.ac.uk

Course description
A description of the state of the art of automated proof using mathematical induction. It will include: an introduction to inductive proof and its applications, especially to system development; an explanation of the theoretical limitations of inductive proof and their practical effects on automation; and the special search problems that arise in automating induction and some attempted solutions to them. The latter will include work at Edinburgh on proof planning and rippling. Proof planning is an attempt to guide proofs using a global strategy rather than local heuristics. Rippling is a particular strategy for guiding rewriting.

Prerequisites
None

Literature
http://www.dai.ed.ac.uk/staff/personal_pages/bundy/esslli-98/esslli-98.html

HOME PROGRAMME CONTACT REGISTRATION

Logic and Computation	AUTOMATING INDUCTIVE PROOFS
Advanced course	ALAN BUNDY Department of Artificial Intelligence, University of Edinburgh
First week	A.Bundy@ed.ac.uk
Course description	A description of the state of the art of automated proof using mathematical induction. It will include: an introduction to inductive proof and its applications, especially to system development; an explanation of the theoretical limitations of inductive proof and their practical effects on automation; and the special search problems that arise in automating induction and some attempted solutions to them. The latter will include work at Edinburgh on proof planning and rippling. Proof planning is an attempt to guide proofs using a global strategy rather than local heuristics. Rippling is a particular strategy for guiding rewriting.
Prerequisites	None
Literature	http://www.dai.ed.ac.uk/staff/personal_pages/bundy/esslli-98/esslli-98.html