Published in Philosophy and the Computer, Leslie Burkholder (ed.) Westview Press, 1992, pp. 213-217.

DEEP THOUGHT (DT) and JUSTIFIED THOUGHT (JT) are programs that have been used for several semesters in teaching deductive proof construction with propositional logic.  DT provides standard proof checking capabilities while JT drills students on rule applications.  What makes the programs distinctive is the way in which they support research into the types of difficulties students have in learning to construct proofs.  As students use these programs, data is collected for identifying and categorizing the most frequent types of errors made.  This information is then used to guide program design and various instructional activities. The programs thus serve to integrate research and teaching.

     Recently, efforts have begun to provide a graphic, mouse-driven interface for these programs.  The interface is still at the prototype stage but is mostly complete for problems requiring only the application of inference (implicational) rules.  Interestingly enough, issues of interface design have begun to interact with issues of integrating research and instruction.  Any program interface forces a certain kind of human-machine interaction, and in the context of CAI, that interaction may facilitate or hinder, highlight or obscure, student thought processes.  This point can be illustrated by describing some of the limitations of the old linear format proof representation and the keyboard-driven interface.  Previously, all interaction with the program occurred via the keyboard, and proofs were represented on a series of numbered lines or steps leading from premises to conclusion.  New steps were generated by typing in logical expressions plus rule names and the appropriate line numbers.  This format was both tedious and error-prone.  The earlier linear format of DT, even while supporting a primitive working backward technique, was not conducive to real-time problem solving.  Consequently, students often did the important work away from the computer and then used the program only for verifying the results of those efforts.  In addition, erroneous line number references were frequent enough to cause difficulties for student error analysis.  Attempts to use the program as a means of investigating actual student efforts as they occur were thus impeded.    Our aim in designing the new interface has been to faciitate proof construction in a way which provides a context for empirical study.  We suspect that we have a long way to go in achieving this goal, but our progress thus far is described below.

     Graphic 1 shows the basic components of the interface and its display.  Standard pull-down menus for various operations are provided at the top of the display.  Two windows are open initially.  The larger window on the left contains a graphic representation of the proof problem.  Premise expressions are displayed at the top of this window while the conclusion appears at the bottom.  Premises are enclosed in bold rectangular shapes and this feature will apply to any expression generated from the premises or any other justified expression.  By contrast, the conclusion, as yet unjustified, is enclosed by a faint rectangle and is marked by a small nodule containing a question mark.

     A second window to the right of the problem window, called the rule palette, provides access to the logical rules of transition.  The definitional form for each rule can be viewed by double clicking the appropriate rule button.  Rules are applied by first selecting the appropriate logical expression(s) and then the rule to be applied.  An illustration of this process is given in Graphic 2.  The two darkened expression nodes have been selected for use and the rule 'MT' is about to be applied.  The results of applying a rule can be seen from previous applications, for example, where 'N' was generated by DS from 'QvN' and '~Q', and where MP was used to produce '~S.'

     This interface also supports the working backwards approach to proof construction.  This feature is implemented by holding the mouse button down on the small nodule attached to the conclusion.  Upon doing this, a pop-up menu appears listing the rules available.  Selecting the rule, MT, for example, produces the results shown in Graphic 3.  The unjustified nodule is removed from the conclusion and replaced by lines leading to the expressions which are required if the conclusion is in fact to be generated by the chosen rule.  These expressions themselves are as yet unjustified and thus contain the appropriate nodules as well as the faint rectangular boundaries (which characterize the conclusion still).

     Given the capability of working forwards and backwards simultaneously, the graphic representation of the growing proof can become quite complicated.  The problem window is scrollable and this feature is useful when premises and conclusion can no longer be displayed simultaneously.  Another capability, however, is to have two problem windows open, one for working forwards and one for working backwards.  The rule palette can be dragged to either side depending upon where work is occurring.  While the two problem windows exist side-by-side, they actually display different portions of the same proof, and activity in one window may affect the display in the other.  Another point of interest is the button, INST, on the rule palette.  INST allows expressions that contain statement forms to be instantiated with particular expressions. As shown in graphic 3, varialbles are represented with geometrical shapes.  Instantiation of variables can be accomplished by selecting  'R > S' along with 'R > Æ' and ' ~S' along with  ' ~Æ' which would have the effect of substituting 'S' for 'Æ'.  While INST is not a standard feature of inference/replacement rule sets, it facilitates the process of working backwards, and any effective use of that process may require some equivalent feature.

     As previously noted, it is hoped that this interface will facilitate the study of student proof construction procedures.  We have already learned something concerning student difficulties with rule applications and hope to learn more in respect to the process of working backwards and of working alternatively in different directions.  One interesting feature of the way proofs unfold in this system is that there is little difference, representationaly speaking, between working foward and working backward.  Previously, a student might sketch out a working backward diagram separately and then use that sketch as a guide to providing the proof.  In the current design, the working backward structure itself is part of the proof.  Hopefully, this will simplify the use of the working backward technique, and with such structures easily built, deleted, and modified, students may be encouraged to use this technique and to simultaneously afford opportunities to observe their uses and misuses of it.

     The JT program has a similar looking interface, and it should be noted that its service in inculcating rule application proficiency has paved the way for ease of rule application in DT.  The target date for full operation of these programs is the Fall of 1990.