Algebraic Manipulation Assistant for Propositional Logic Rein Prank, Hellis Viira Computer Science Department Tartu University 2, Liivi Street Tartu 202400 Estonia, USSR At the end of 1987 in Tartu University a software project for exercises on Elementary Mathematical Logic was started. At the first stage we designed four programs for the following types of exercises: 1.Truth-table exercises (tautologies, equivalence etc.). 2.Algebraic manipulation of formulas (normal forms, expressi- bility in terms of {&,ª), {v,ª} and { ,ª} etc.). 3.Proofs in Gentzen Type Propositional Calculus. 4.Construction of Turing Machines. Having no experience of the use of computers in the teaching of mathematics, we have not tried to implement the programs from the beginning in the maximal possible generality. For instance, the Algebraic Manipulation Assistant and Proof Editor are written only for Propositional Logic. The first versions of the programs listed above are now in exploitation, and we have designed and partially implemented the next stage. As we have supposed, the only program, which will be essentially changed, is the Algebraic Manipulation Assistant. In the following article we discuss our experience of work with the first version of Algebraic Manipulation Assistant and describe the user interface of the second version. Š 1.First Version of Algebraic Manipulation Assistant Our first program for formula manipulation exercises (written by H.Viira) is implemented for exercises on disjunctive normal forms and expressibility in terms of {&,ª}, {v,ª} and { ,ª}. The user has a choice of three modes of manipulation: 1)AUTOMATIC Mode (by program), 2)STEPWISE Mode (with checking after any conversion), 3)TEST Mode (with checking at the end of work). More precisely, the work in Modes 2 and 3 is carried out as follows. The student enters his transformation line by line. The input is controlled by a special editor which ignores the symbols (keys) not allowed for formulas, ignores the difference between upper/lower case, supports the input of propositional connectives using functional keys and allows to copy the non-changed pieces of the last formula. The input of any step is terminated with "=" (if the transformation is not finished) or with ";" (if the stu- dent supposes that the goal is reached). After an input of "=" or ";" the program checks the syntax of the entered formula. If the formula is syntactically incorrect, the diagnostical message is given and the student has to correct the formula. In the TEST Mode the step is ended if the formula is syntac- tically correct. In the STEPWISE Mode the program also checks 1)the equivalence with the preceding formula, 2)profitability of the last step (partially), 3)if the goal is reached or not, and gives the corresponding messages. In case of the non-equiva- lence the student must correct the formula. The message about un- Šprofitability is considered as a warning and the student can either correct the formula or continue. If the symbol "=" or ";" does not agree with the situation, the program terminates the transformation or demands the continuation. In the TEST Mode the last three tests are made only when the process of the solution is terminated with ";". In both of the modes the program has counters for syntax, equivalence, profita- bility and termination errors. The result of the finished or non-finished transformation can be saved in the file or loaded from the file. The Help-function gives information about the algorithm of transformation for the exercise and about the identities necessary for the next step. 2.Disadvantages of the First Version and the Ways of Overcoming Them From the theoretical point of view, the weakest part of the First Version is the control of the profitability. On many occa- sions the possibility of arbitrary transformations of arbitrary parts of the formula makes the program abandon the diagnosis and all the testing is reduced to the checking of the equivalence with the preceding formula. The problem could be solved better and easier if the student had at any step to point out separately the part of the formula to be converted and the conversion it- self. The second weak point is the symbolwise typing of the formu- las. Our first-year students have too little practice of the work on the keyboard and often make only partial use of the whole ca- Špacity of the editor. We must limit the size and the complexity of students' input. We also know that we cannot use the approach described above for the Predicate Calculus because the unsolvability of the equi- valence of the formulas. The most radical solution of those problems is to replace the symbolwise input of the formulas with the rule-oriented control over the manipulation. By such an approach the student at any step of the work points out a subformula and selects for conver- sion of this subformula one of the identities from the menu on the screen (for instance, ªªX=X or ª(X&Y)=ªXvªY. The program checks up if the use of this transformation rule is possible, and puts the result on the screen. The choice of the subformula can be made by means of the Subformula Locator, widely used in the interactive expression manipulation programs. The "active" sub- formula has the highlighted background on the screen, and some keys (for instance, arrows) move the "activity" to the left/ right neighbour and to the subformula/superformula in the analy- sis tree of the formula. The operating scheme described here greatly simplifies the input. The students' attention is now concentrated on the general algorithm of the transformation and the details may be ignored. The checking of profitability is also simplified, since the stu- dent almost explicitly refers to the meaning of the step. But we cannot forget that in such a mode an essential part of the work is made by the program and, accordingly, the student has no possibility to make some typical errors: misunderstanding of the priority of the propositional operations, applying some invalid Š "identity", omitting the necessary brackets around the changed subformula. For training and testing of these aspects of manipulations the Assistant can have the intermediate (in the sense of the com- plexity of the input) modes where: a) the Subformula Locator is moved linearly by shifting the left and the right ends (instead of jumps on the syntax tree), b) the new string replacing the highlighted subformula is en- tered directly by the student or is defined by a transformation rule entered by student. 3. The Second Version The Second Version contains an Editor for exercise files and typically the program loads the exercise from the file. The exer- cise is defined by the following parameters: 1) the type of the problem (DNF/&ª/vª/.../FREE), 2) the given formula for transformation, 3) the global work mode (AUTOMATIC/STEPWISE/TEST), 4) subformula locating mode (LINEAR/TREE), 5) subformula replacing mode (RULE/INPUTRULE/IMMEDIATE). The set of the available problem types is fixed by program configuration. For any type the program contains the automatic solution procedure, on-line help, profitability grading procedure and termination checking procedure. Correspondingly, for each new type a unit with these procedures must be added. The teacher can give all the transformation problems, not included in the current set of types, to solve under type FREE. This type does not have Š the AUTOMATIC mode and the program does not check the profit- ability and finish (i. e. only syntax and equivalence are checked). The formula can be read from the exercise file or entered from the keyboard or generated by random formula generator. The global work modes are those of the First Version and the local work modes are described in Part 2. Within one step of transformation the user can transform in parallel more than one subformula provided that these subformulas are not nested. The parts of the formula not transformed (not highlighted) are always automatically copied to the next line. 4.Subformula locating We have tried to make the work of the student close to the formula manipulation on the paper. Therefore we cannot consider the disjunction and conjunction only as binary operations. We also do not fix the tree structure of the formula containing the n-ary disjunctions or conjunctions. The program accepts arbitrary segment of a n-ary junction as a subformula. In LINEAR mode such a subformula can be located as arbitrary substring of the formula. In TREE mode the arrow keys move the "activity" among the n-ary tree and the and keys add the left/right neighbour to the highlighted segment of the n-ary junction. Š 5.Subformula replacing modes The IMMEDIATE Mode is in fact the string replacing mode from Version 1, applied to subformulas. The student enters the string to replace the selected subformula. The program checks the syntactical correctness, the equivalence of entered expression with the old subformula and the use of parentheses (for instance, the student must enter (ªXvªY) but not ªXvªY to replace ª(X&Y) in Z&ª(X&Y)). The RULE Mode is the second basic mode. Having fixed the sub- formula for conversion, the student selects the conversion rule from menu. The following list presents the menu for problem type DNF. The rule sets for other types are similar. 1.X÷Y = X&YvªX&ªY 7.Xvf = X 2.X-Y = ªXvY 8.XvX&Y = X 3.ª(X&Y) = ªXvªY 9.X = X&YvX&ªY 4.ª(XvY) = ªX&ªY 10.(X) = X 5.ªªX = X 11.X*X = X 6.X&(YvZ) = X&YvX&Z 12.X*Y = Y*X 13.X*(Y*Z) = (X*Y)*Z The Rules 11-13 can be applied to conjunction or disjunction. The issues 1-6 in the list present also more than one rule. The program gives a possibility to modify the "activated" rule by functional keys. The F1 key applies the negation to the both sides (for example, the first rule is changed to ª(X÷Y) = X&ªYvªX&Y) and the F2 key exchanges the sides of the rule (the modifications work only where it is reasonable). When the choice is made, the program checks if the applying of the selected rule is possible. If not, the error message is given and the student can select the other rule or subformula. According to our paper-and-pencil approach we have implemented the rules concerning disjunction and conjunction so that they may be applied to n-ary junctions. In case of the rules from the right column we also permit the multi-use of the selected rule in one step (deleting more than one member by Rules 7,8 and 11, adding more than one variable by Rule 9, arbitrary reordering by Rule 12 and arbitrary changes of the brackets by Rule 13). In many ocassions it causes no new problems (for in- stance, Rules 3,4 and 6). When the result of the application of the rule is not clear, the student is asked about additional information. So, in case of Rule 7 the student is asked about each member of disjunction, whether to delete it or not. Then the program verifies whether the members to be deleted are false, and that not all members are deleted. Using Rules like 7, 8 and 11, the program allows to delete the members only in accordance with the meaning of the rule. For instance, by Rule 11 we can convert X&Y v X&Y v X v X&Y v X to X&Y v X but not to X. The last step can be made by Rule 8. The INPUTRULE mode is intermediate between IMMEDIATE and RULE Modes. The student manipulates the formula as in RULE Mode using the rules from menu. Some rules (like 10-13) are from the beginning on the screen. The student can add new rules and delete them. By input of a new rule the program verifies the equivalence of the left and the right sides. If the entered rule is identical to some rule realized in the program, the program will understand it in an equal way. Otherwise the rule will be applied purely syntactically. 6.Conclusion The two versions of Algebraic Manipulation Assistant for Pro- positional Logic have brought us to quit universal operating schema for the drill of work with expressions. Not all work modes described above can be used for arbitrary classes of expressions. We can use only the rule-based replacing modes if the equivalence of the expressions is unsolvable as in the case of Predicate Logic, or if it is solvable, by some noneffective algorithm. In some cases this barrier can be exceeded using a checker which accepts any conversion only if it is able to prove its correct- ness in some reasonable time amount.