| ||||||||||||

## Workshop web page with more informationhttp://www.dai.ed.ac.uk/homes/simonco/conferences/CADE02/## PurposeThe purpose of this workshop is to discuss the role of automated deduction in all areas of mathematics. This will include looking at the interaction between automated deduction programs and other computational systems which have been developed over recent years to automate different areas of mathematical activity. Such systems include computer algebra packages, tutoring programs, systems developed to help explore a mathematical theory, and those developed to help present and archive mathematical theories. The workshop will also include discussions of the use of automated theorem proving in the wider mathematical community. Presentations which detail the employment of automated deduction techniques in any area of mathematical research are encouraged. We are interested in the interaction of automated theorem proving programs with (i) computer algebra (CA) packages (ii) constraint solvers (iii) model generators (iv) tutoring systems (v) interactive textbooks (vi) theory formation programs and (vi) mathematical databases. In all these fields automated deduction is either already used or could be fruitfully employed to enhance the power and reliability of existing systems. Particular ongoing projects include the use of deduction to certify CA systems, and also to enhance CA systems. Other projects include the incorporation of deduction into mathematical tutoring systems and interactive mathematical textbooks and the use of theory formation to help in automated theorem proving and constraint satisfaction problems. The interaction between these programs could be in terms of improving automated deduction or in terms of using automated deduction to improve the techniques employed in the other system. The workshop is intended to inspire the use of automated deduction within other fields of mathematics as well as the incorporation of techniques from other fields into automated deduction. The workshop will provide a forum for discussion between researchers interested in various aspects and application areas of mathematics, with particular emphasis on the role of automated deduction. ## SubmissionsOriginal workshop papers of up to 10 pages are solicited which discuss the interaction of automated deduction and other mathematical techniques, including, but not restricted to:- computer algebra
- constraint solvers
- model generators
- theory formation programs
- mathematical tutoring systems
- mathematical textbook systems
- mathematical databases
We also hope to attract papers discussing the use of automated deduction for mathematical research, including, but not restricted to: - The use of automated theorem proving on particular problems from mathematics.
- The use of semi-automated deduction techniques in mathematics.
- Novel frameworks for the use of automated deduction within mathematics.
## Invited speaker- John Harrison, Intel, USA
joint with PaPS:*Extracting test problems from real applications*
## Panel- Peter B. Andrews, Carnegie
Mellon U, USA; Alan
Bundy, U Edinburgh, UK; William McCune, Argonne National Laboratory, USA; and Rick Sommer, Stanford U, USA
joint with PaPS:*Challenge problems for automated deduction (with special emphasis on mathematics)*
## Organizers- Simon Colton <simonco@dai.ed.ac.uk>, U Edinburgh, UK
- Volker Sorge <sorge@ags.uni-sb.de>, Saarland U, Germany
| ||||||||||||

| ||||||||||||