Rein Prank Dept of Computer Science Tartu University 2, Liivi Str. EE2400 Tartu Estonia e-mail: prank@csd.ut.ee ------------------------------------------------------ Published in: Informatik und Schule 1991, GI-Fachtagung Oldenburg 7.-9. Okt.1991 Informatik-Fachberichte, 292, 34-38. Springer-Verlag, 1991 USING COMPUTERISED EXERCISES ON MATHEMATICAL LOGIC Rein Prank Introduction At the end of 1987 we started a teaching software project for the Basic Course on Mathematical Logic for first-year students. The decision to use the computers was initially caused by poor performance of the students in two subjects: programming Turing Machines and the construction of the proofs in formal theories. In the process of the work we have added two more simple themes: truth-table exercises and the algebraic manipulation of the formulas. Our approach to the computerisation of teaching can be characterised as quite conservative. We have written programs only for the exercises (of course, they can also be used for the demonstrations and for tests). We have decided (at least in the first steps) to computerise only the exercises, having been used in our work before the use of computers, and not to introduce any new types of the problems. We have also tried not to change the role of the student in the solution of the problem. So we have not used the Computer Algebra Programs which enable formula manipulations without intellectual participation of the student or Resolution Provers. Using our programs the student has mainly three possible roles. In the simplest occassions the role of the student is equal to his role by the work on the paper (filling a truth-table with the symbols 't' and 'f' or writing the formula manipulation step by step). In some other cases the student has to explain (in usual mathematical terms) to the computer what to do next. For in- stance, he has to fix the part of the formula to be changed in the next step and to enter (or to select from the menu) the rule for this change. In case of TURING MACHINE the student works like a programmer who is editing, testing and debugging the program. From 1988 we have worked with the students in the computer classroom with eight or ten IBM PC compatible computers. The greatest problem has been the sharp deficit of the computer time. The computers have been used almost only for the exercises under the supervision of the teacher (two hours per week) and for the tests. From March 1991 we have new classrooms with 16 PC and in the last term beginning from Chapter III (see below) our students have had the time for independent work on computers. 1. The Basic Logic Course and the Programs The main content of the course is presented in the following table. ----------------------------------------------------------------- Chapter | Lectures (hours) | Exercises (hours) ----------------------------------------------------------------- I. | Introduction. Sentences, | Reading formulas, writing Propos. | truth-values, connections, | sentences by formulas. (1) logic | formulas, truth-tables. (2)| | Tautologies,satisfiability,| Truth-tables, tautologies, | logical equivalence. (2)| satisfiability, logical | | equivalence. (2) | Normal forms. (2)| Expressibility by {&,ª}, | | {v,ª}, {->,ª}. (1) | | Normal forms. (2) | | Test. (1) ----------------------------------------------------------------- II. | Predicates,quantifiers. (2)| Validity of formulas on Pred. | | N,Z,R,P(N), writing logic | Signature, first-order | predicates and theorems | language, interpretation, | by formulas. (2) | theory of a model. (2)| | Logical equivalence. (2)| Prenex form. (2) ----------------------------------------------------------------- III. | Axioms and rules of | Proofs in Propositional Axiom. | Propositional Calculus. | Calculus. (4) theories| Examples of the proofs. (2)| | Consistence and complete- | | ness of Prop. Calc. (3)| | Predicate Calculus. (3)| Proofs in Predicate | First-order ax. theories, | Calculus. (4) | Formal Arithmetic. (2)| Test. (2) ----------------------------------------------------------------- IV. | Turing Machine. Computing | Programming TM for Algor. | arithmetical functions on | arithmetical functions.(2) Theory | TM. (2)| Test. (2) | Enumeration of TM. Halting | | Problem. (2)| | Decidable and | Decidable and | enumerable sets. (4)| enumerable sets. (2) | Decidability and enumer- | | ability in Logic. (2)| The classroom exercises are solved in groups of 20..25 stu- dents. Earlier the number of participants of our computerised exercises has been depending on the type of the tasks (one or more students for a computer). Our work in the last term demon- strates that the classroom exercises can be solved with two students per computer if they are followed by independent work on computer. At the present stage we have implemented programs for four types of the exercises: 1.TURING MACHINE (exploited from spring 1988). Turing Machine programming environment. 2.ALGEBRAIC MANIPULATION ASSISTANT (autumn 1988) for propositional formulas. 3.PROOF EDITOR for the proofs in Gentzen Type Systems (spring 1989 Propositional Calculus, spring 1991 Predicate Calculus). 4.TRUTH-TABLE CHECKER (autumn 1989). In addition, we use a formula generator allowing to gener- ate a given number of propositional formulas with given parame- ters (the choice and numbers of variables and connections) for individual tasks. In the near future the predicate version of Program 2 will be ready for exploitation. The programs are writ- ten in Turbo Pascal (3.0 and 5.0). Below we shall discuss the use of the programs in the several parts of our course. Some attention will be paid to two tactics of saving the computer/teacher time: a) collective work with one computer, b) work in two steps: preparing the solution on paper and then checking it by using the computer. 2. Propositional Logic (Chapter I) We are working with two programs for the exercises on Propositional Logic. The TRUTH-TABLE CHECKER supports the exercises on filling the truth-table, checking tautologicity, satisfiability and equivalence of the formulas, finding the formula for the given Boolean function. The work of the student at the task consists normally of two parts: filling the table and the answer motivation dialog. In the case of the find-formula problem type the filling part is the last. The student can switch over to the answer when he supposes that the answer can be motivated using the entered values in the table. In all the types the student can return from second part to the first. The program has the counters of mistakes in order, values and answer. The task in the exercise file can contain the following items (only the first is obligatory): exercise type (TTABLE/ TAUTOL/ SATISF/ EQUIV/ FINDFORM), text, formula(s) or vector of values, options of table filling regime. The formula can be replaced with GENER with parameters for random generator or INPUT. The regime options are LINEFILL (FULL/ PARTIAL), ORDER (CHECKED/ FREE/ AUTOMAT), OPERATIONS (STUDENT/ AUTOMAT), VALUES-CHECKING (RAPID/ BEFORE_ANSWER/ AT_END). The wide spectrum of the regimes is necessary for sporadically contradictory applications. The default regime is FULL + CHECKED + STUDENT + BEFORE_ANSWER. The first exercises are made by RAPID values-checking. The student's "debugging" of the written home-work can be made by using PARTIAL+FREE or even OPERATIONS=AUTOMAT. Some combinations of the options are planned for the teacher's work by preparing the exercises or the correction of written tests. The ALGEBRAIC MANIPULATION ASSISTANT is used for the tasks on expressibility in terms of {&,ª}, {v,ª} or {->,ª} and normal forms. The student makes his transformations step by step. Our first version worked using student's direct input of the formulas. In the second version (described in [4]) any step is split in two substeps: the student has to point out a subformula and then define the transformation of this subformula. The location of subformula can occur in two modes: LINEAR (shifting the ends of "activated" substring) or TREE (using jumps on the syntax tree). The subformula replacing modes are RULES (selected from the menu), INPUT_RULE and IMMEDIATE (input). Consider now our exercises as they have been organized having no possibility of computerised home-work. We have supposed that the first exercises on understanding of logical connections and the formalization of logic as such are more efficient in dialog with the teacher. We have not attempted to computerise them and so during the first two hours the stu- dents are working in the classroom. After the exercises on read- ing and writing we consider the tautologies and satisfiability. At the end some simple tasks on finding the formula with given values are solved. The students get home-work of this type. The second lecture contains a great number of equivalence claims given without proof. The first work on computer is verification of them by CHECKER. Then the formulas constructed at home are verified. The use of MANIPULATION ASSISTANT is introduced using each of pairs {&,ª}, {v,ª} and {->,ª} to express all the remaining connections (in INPUTRULE mode, using the equivalences from the lecture and the expression rules proved already). The further expressibility exercises are made in LINEAR + INPUTRULE (to emphasize the order of operations and remembering rules). The third lecture contains, in addition to the theoretical results, the algorithm of transformation to DNF illustrated with examples. The first examples on computer are solved in TREE+RULES accentuating the general algorithm. The home-work given at the lecture is verified in LINEAR+IMMEDIATE. After that the conjunc- tive NF is considered. The test (60 minutes) has been organized using a special time-table. It consists of three tasks with the formulas contain- ing three variables and all the five connectives: 1) verifying the equivalence, 2) expression by one of the pairs (LINEAR+INPUTRULE), 3) DNF (TREE+RULES). The organization of the work on Chapter I has been quite difficult. The exercise classes have obtained some leading role and we had to synchronize the lectures with them. The work in pairs with one computer without additional independent work has given poor results. The weaker students are still passive and do not get the formula editing and manipulation skills. The first chapter contains a lot of new, but fairly easy concepts. The student's need of computer time is very individual here. 3. Predicate Logic (Chapter II) Up till now we have not used the computers in Predicate Logic. The computerisation of Model Theory has well-known unsolvability and complexity restrictions. Starting our project we simply did not have any ideas for overcoming them. Barwise and Etchemendy [1,2] in their very interesting TARSKI'S WORLD have used finite models. But not all the aspects of the course can be carried out this way. At the present stage we continue to follow the traditional technology. The prenex form exercises do not differ essentially from formula manipulation exercises on Propositional Logic. We intend to put them in the computer in the autumn term of 1991 using the new enhanched version of ALGEBRAIC MANIPULATION ASSISTANT. 4. Axiomatical Theories (Chapter III) In the exercises of this chapter we have been dealing with the proofs in Propositional Calculus of [3] having the following inference rules: gÃA; gÃB g,A,BÃC gÃA gÃB g,AÃC; g,BÃC g,AÃB -------- ------- ----- ----- ------------ ------ gÃA&B g,A&BÃC gÃAvB gÃAvB g,AvBÃC gÃA->B gÃA; gÃA->B g,AÃB; g,AêB gêªA gÃA g,A,B,EÃC ----------- ------------- ----- ----- --------- gÃB gêA gÃA g,BÃA g,B,A,EÃC Such Gentzen Type system seems to be a reasonable compromise between the simplicity of finding the proofs and the simplicity of the objects considered. In Gentzen's original sequential system the proofs can be found by a very simple algorithm. But the sequents with more than one formula in the right side are objects without clear semantics. On the screen of the PROOF EDITOR the proofs are built in the form of the tree from the root upwards (from the sequent to be proved to the axioms). At any step the student has to select an inference rule from the menu. The program checks if the application of this rule is possible. If not, the corresponding message is given. Otherwise the upper sequent(s) of the rule is (are) added to the tree. If the upper part of the rule contains a new formula, the student has to enter it. The program checks when the proof is complete. The proofs (completed or not) can be saved to file, loaded from file or printed. The students have to prove about 40 sequents. Any valid sequent can be proved in our system combining Gentzen's general tactics (splitting all formulas in components) with two addition- al ones (proving the sequents of form A,ªAÃB and ÃAvªA). The examples are built up in three cycles: splitting, simple cases with negation or modus ponens, combined tactics. Each of the cycles is introduced by teacher's explanation. In the spring term of 1991 we have added the exercises on Predicate Calculus containing about 30 sequents. The teaching tactics was similar to Propositional case. The tests on building proofs have given unusually good re- sults. 5. Algorithm Theory (Chapter IV) The programming environment TURING MACHINE consists of a special Editor for Turing Machine tables (as they are defined in Kleene's "Introduction to Metemathematics") and an Interpreter. The Interpreter allows us to run the Machine with the user given input data and to demonstrate the work on the tape stepwise, as well as in three more quicker regimes. The program saves all the tests runned together with the result of running (OK, wrong result or error message). The tables can be saved in text file and loaded from file. We have not set ourselves the goal of teaching students to write programs for hard problems in Turing Machine language. The first problems are like computing f(x)=c and the hardest are on the level of division and multiplication. They are all directed to right understanding of the computing of numerical functions with several numbers of arguments rather than to programming. The first examples of the Machines and some hints about programming are given at the first lecture. The students get some common and some slightly varying individual problems (for in- stance, to compute the function f(x,y)=ax+by+c with individual a,b,c). The computers are used mainly for testing and debugging of the Machines constructed at home on paper. The programming tasks are quite suitable for the work in pairs. In case of an individual task the Machine of the second student can be received from the table of the first by appropri- ate correction. The realization of such a correction by Editor is typically quite easy. So, the input of two tables does not take double time and, moreover, the students have a real reason for thinking about some generalization of their solutions. The exercises on decidable and enumerable sets are not com- puterised and we do not intend to computerise them. References 1.Barwise, J.; Etchemendy, J.: Creating Courseware. Notices Amer. Math. Soc. 36, 32-40 (1989). 2.Hodges, W.: Review: TARSKI'S WORLD AND TURING'S WORLD. Computerised Logic Teaching Bulletin 2, Nr. 1, 36-50 (1989). 3.Kolmogorov, A.N.; Dragalin, A.G.: Introduction to Mathematical Logic (Russian). Moscow Univ. Press, 1982. 4.Prank, R.; Viira, H.: Algebraic Manipulation Assistant for Propositional Logic. Computerised Logic Teaching Bulletin 4, Nr. 1, 13-18 (1991).