Special issue of Journal of Automated Reasoning

Since the advent of type inference in ML, there has been an intimate
connection between algorithms for types checking and type inference
and automated deduction algorithms. Further, the implementation
of logic programming languages use automated deduction algorithms.

The following call requests papers relating automated deduction algorithms
(which could be used in the context of programming language implementation)
and education.

                               Call for Papers

                Special Issue of the Journal of Automated Reasoning

            Automated Reasoning and Theorem Proving in Education


                              Deepak Kapur
                        University of New Mexico

During the past ten years, theorem proving has been playing
an increasingly important role in education.
One reason is the improvement in the "friendliness" of theorem provers;
many are now suitable for the nonspecialist and produce quite readable proofs.
Another is their demonstrated success in solving 
not only "toy" problems but previously open questions in mathematics and logic.
In light of these developments, we plan a special issue of
the Journal of Automated Reasoning, ARTE, on
the use of theorem provers in education at all levels.

Possible topics include the following:

  * Automated reasoning for mathematics and logic education
  * Mathematical tutoring
  # Geometry and theorem proving

  * Business education, statistics, and theorem proving
  * Theorem provers developed specifically for teaching

  * Educational games and theorem proving

  * Comparisons of theorem provers and symbolic systems

  * Web-based theorem provers for learning over the Internet

  * Automated courses 

  * Theorem provers and education -- whence and whereto

We welcome contributions about experiences using automated theorem 
provers for education at all levels:
from elementary and secondary school to college and university and beyond.

Our focus is not on the use of theorem provers in classes specifically
devoted to the teaching of theorem proving or automated reasoning.
Rather, we are especially interested in discussion of the benefits (or problems
encountered) in using automated theorem proving technology to
motivate students and to enhance their ability to understand new topics.

Prospective contributors are welcome to contact
the editor to discuss the suitability of topics and papers.

Please send 3 copies of your manuscript or (preferably) a postscript file to:

           Dr. Deepak Kapur
           Chairperson, Computer Science Department
           University of New Mexico
           Albuquerque, NM  87131
           E-mail: kapur@cs.unm.edu

Please also send one copy to 

           Dr. Gail W. Pieper
           Managing Editor, Journal of Automated Reasoning
           Mathematics and Computer Science Division
           Argonne National Laboratory
           Argonne, IL  60439
           E-mail: pieper@mcs.anl.gov

Submission deadline               December 10, 2002
Notification                      May 10, 2003