Stanley N. Burris, Department of Pure Mathematics, University of Waterloo, Waterloo, Ontario, Canada, N2L 3G1 email: snburris@thoralf.uwaterloo.ca Special Session: Education Title: Computer enhancements to my course "Logic for Mathematics and Computer Science" Abstract: This talk will focus on the software that I use in conjunction with the course in logic that I have taught several times at the university of Waterloo. The object of the course is to combine the traditional treatment of logic with the logic needed in automated theorem provers such as "Otter". I wrote a number of simple interactive web programs that I use to demonstrate key ideas, and these will be discussed in my talk. --------------------------------------------------------------------------- Wilfried Sieg, Department of Philosophy, Carnegie Mellon University, Pittsburgh, PA 15213; e-mail: sieg@cmu.edu Special Session: Education Title: Computer based logic instruction Abstract: I will talk about two related projects that have been pursued at Carnegie Mellon for more than a decade. The first project, VALID, is based on an introduction to logic that was developed at Stanford up through the early 1980s, by Patrick Suppes and collaborators. This is a "classical" introduction to first order logic; it has been thoroughly revised and is now fully web based. The second project, APROS (Automated PROof Search), provides the framework in which VALID students can construct natural deduction proofs. The distinctive and pedagogically very effective feature is that they can work "forward" and "backward." APROS, guided by logical strategies, searches itself for natural deduction proofs; I will describe our attempts to use APROS as a tutor providing systematic help to students and also (plans for) a new course in which proof construction takes center stage. --------------------------------------------------------------------------- Daniel J. Velleman, Department of Mathematics and Computer Science, Amherst College, Amherst, MA 01002-5000, email: djvelleman@amherts.edu Special Session: Education Title: Proof Designer: Software for learning to write proofs Abstract: I will demonstrate a java applet called Proof Designer that is intended to help students learn to write proofs. Proof Designer acts as a "referee" while the student tries to construct a proof in elementary set theory. Proof Designer allows the student to choose from a variety of proof strategies and rules of inference, but it refuses to tolerate incorrect reasoning or nonsense. Proof Designer can be found at http://www.cs.amherst.edu/~djv/pd/pd.html.