stevens@ANL-MCS.ARPA (Rick L. Stevens) (04/22/87)
Automated Reasoning Workshop 1987
Mathematics and Computer Science Division
Argonne National Laboratory
You are invited to a workshop on automated reasoning to
be held at Argonne National Laboratory on June 23 and 24,
1987. This workshop, the sixth of its kind, will take the
form of a set of tutorials. No background is needed in
automated reasoning, simply curiosity and an interest in the
subject.
Our first objective is to acquaint people with the
basic aspects of automated reasoning and with the possible
applications. Thus we shall discuss some of the previously
open questions we have solved and feature topics such as the
design of logic circuits, the validation of existing circuit
designs, and proving properties of computer programs. Our
second objective is to learn of new problems on which the
current methodology might have an impact. In fact, the
preceding workshops did lead to such discoveries, as well as
to collaborative efforts to seek solutions to these prob-
lems.
Enclosed is a tentative schedule that briefly describes
the various talks. On the first day, we shall begin with an
introductory lecture on what automated reasoning is. We
shall illustrate the various concepts first with puzzles.
Next, we shall focus on some applications of automated rea-
soning. We shall include a demonstration of an automated
reasoning program (ITP) that is portable, runs on relatively
inexpensive machines, and is available to other users. On
the second day we shall give an introduction to Prolog, dis-
cuss additional applications, and focus on state/space prob-
lems. On both days, we have scheduled reviews of the
material and open discussions.
We welcome you to this 1987 workshop on automated rea-
soning. Participation will require a small charge, no more
than $60. Included in this fee will be the cost of the book
Automated Reasoning: Introduction and Applications, written
by Wos, Overbeek, Lusk, and Boyle and published by
Prentice-Hall. This book covers the field of automated rea-
soning from its basic elements through various applications.
Its tutorial nature will guide our approach to the workshop.
We urge you to respond to this invitation as soon as
possible for, to retain the tutorial atmosphere of the
workshop, we may be forced to limit the number of partici-
pants. The order in which requests are received will be an
important parameter in issuing invitations to attend the
workshop.
Sincerely,
L. Wos
Senior Mathematician
Schedule for Automated Reasoning Workshop 1987
June 23-24, 1987
Argonne National Laboratory
Argonne, Illinois
Tuesday, June 23
9:00 - 9:15 Preliminary remarks - Larry Wos
9:15 - 10:15 Introduction to automated reasoning
- Larry Wos
10:15 - 10:30 Break
10:30 - 11:30 Solving reasoning puzzles - Brian
Smith
11:30 - 12:30 Lunch
12:30 - 1:15 Choices of strategies and inference
rules - Rusty Lusk
1:15 - 1:30 Demonstration
1:30 - 1:45 Break
1:45 - 2:45 Proving properties of computer pro-
grams - Jim Boyle
2:45 - 3:00 Closing discussion - Larry Wos
Wednesday, June 24
9:00 - 9:15 Discussion - Larry Wos
9:15 - 10:15 Introduction to Prolog - Rusty Lusk
10:15 - 10:30 Break
10:30 - 11:30 State-space problems - Rusty Lusk
11:30 - 12:30 Lunch
12:30 - 1:15 Circuit design and validation - Jim
Boyle
1:15 - 1:45 Open problems in mathematics and
logic - Rusty Lusk
1:45 - 2:00 Break
2:00 - 2:45 Detailed solution of an open prob-
lem in logic - Larry Wos
2:45 - 3:15 Our automated reasoning software -
Rusty Lusk
3:15 - 3:30 Closing remarks - Larry Wos