Writing a proof is a task that requires certain habits of mind. One must be able to fluently switch between taking care of details in a single step of a proof and, simultaneously, keeping the ?big picture? in mind. After all, correct steps that do not lead to the desired conclusion are not useful. In order to write a proof, a trained mathematician uses a multitude of skills that, through long use, may not even be considered skills any more. Proof designer demonstrates proof structure and supports development of the ability to nest sub-steps into a larger picture by automating many of the common starts and endings of sub-steps in a proof. For example, to prove a universally quantified statement we need to pick an arbitrary element and prove the statement for it. In proof designer such steps are created upon selection with the characteristic start ("Let a be ") and the characteristic ending ("Since a was arbitrary "). The user still has to fill in the middle, but the ?bookkeeping? is automatic. This structure allows the reader to focus on a sub-step, without losing the overall structure. The nesting of sub-steps is presented visually with programming language type indentations. Moreover, proof designer will alert the user to possible gaps if a proof is declared to be finished too early. To select the right inference modes etc. the student must be familiar with standard logical terminology, which is another learning goal in a first proof class. Use of proof designer automatically trains the user in the use of this terminology.

Type of Material:

Simulation.

Recommended Uses:

Classroom demonstrations at first. Later also as help on homework in a first proof class or as a part of a take-home assignment.

Technical Requirements:

WINDOWS browser with SUN Java Plugin or Macintosh. The plugin is automatically downloaded from the applet site.

Identify Major Learning Goals:

To write structurally sound proofs.

Target Student Population:

Students learning how to do proofs or ?Introduction to Proofs? course students.

Prerequisite Knowledge or Skills:

Varies. Basic set theory (sets, elements of sets, set operations) is used in the introductory example. However, such basics as well as the standard inference modes and logical notations can also be taught side by side with use of proof designer.

Content Quality

Rating:

Strengths:

The automatic structuring of a proof relieves the novice of the arduous task of keeping track of what level of the proof is currently finished. It thus shows clearly the nonlinear structure of proof-writing by providing starting and ending statements for each sub-step with the middle still left to be filled in by the user.

Concerns:

Statements are limited to the language that the author provides (basic set theory). This should not be a problem, as the tool is intended to help users as they start learning how to do proofs. It is not an oracle for proofs in, say, abstract harmonic analysis.

Potential Effectiveness as a Teaching Tool

Rating:

Strengths:

This applet provides a great demonstration tool for an introductory Logic and Proofs course. It can be used side-by-side with a large chunk of textbook material on proof structures and working proof strategies. Aside from the automatic structuring mentioned above, proof designer will alert the user to possibly missing steps. This instant feedback can make it a good tool for independent use. The user is alerted that there is a gap, but not (like a worked solution would do) as to how to fill it.

Concerns:

Some novices might use proof designer as a crutch, which eventually is a liability rather than an asset. However, the slow input and writing in proof designer should make it clear to all students that use of this tool is an intermediate stage. The intent is to lead the user to having the automatic habits of mind of a mathematician who is writing a proof, not to provide an automatic proof-writing tool.

Ease of Use for Both Students and Faculty

Rating:

Strengths:

After introduction of all the necessary terminology, proof designer should be easy to use and the menus will indeed reinforce logical terminology.

Concerns:

Input remains tedious, but this is a common problem for mathematics. The interface is competitive with commercial interfaces for precalculus that one reviewer has seen. The shortcomings in the input are ascribable mostly to the complexity of the task. The undo function only undoes the last step executed. Given that a proof can go into deeper ?blind alleys?,
a deeper undo function would be desirable. There are other commands that can be used to edit the proof--namely, the Delete and Rejustify commands. Using these commands it is possible to backtrack further if the user decides that there is a mistake several commands back. However, the backtracking is not as simple as it would be if one could undo multiple steps. The Java Plugin used does not open in a separate window which may create a problem if one tries to access it using several open browser windows (for example instruction or sample problem pages).

Creative Commons:

Search by ISBN?

It looks like you have entered an ISBN number. Would you like to search using what you have
entered as an ISBN number?

Searching for Members?

You entered an email address. Would you like to search for members? Click Yes to continue. If no, materials will be displayed first. You can refine your search with the options on the left of the results page.

Searching for Members?

You entered an email address. Would you like to search for members? Click Yes to continue. If no, materials will be displayed first. You can refine your search with the options on the left of the results page.