;;;; Assignment 2 ;;;; ;;;; File: asst2.txt ;;;; Author: CS 51 (Bob Walton) ;;;; Version: 2 The file propositional-calculus.lsp contains a fairly complete set of functions for performing propositional calculus computations in LISP, but unfortunately it is incomplete. Your task in this assignment is to supply the missing rewrite rules and code in this file. You must also test your code using the file propositional- calculus.in. To warm up to this task, you are given some theory exercises from Chapter 2 of Introduction to Symbolic Computing. The specific things you must do are: (0) Read Chapter 2 of Introduction to Symbolic Computing. You may skip the sections on rational expressions (2.4) and proofs (2.6). (1) For the theory part of the assignment, do the following exercises from Chapter 2 of the above reading: 2.1.1.2(b) 2.2.1(b) (labeled 2.2.0.2(b) due to typo) 2.3.4(d) 2.5.1.1(a) 2.5.4.1(a) 2.5.5.2(d) Remember to staple this part separately as it will be graded separately from the code. (2) In propositional-calculus.lsp, write the rewrite rules (RR) for the functions: evaluate theorem?-1 dnf-distribute dnf theorem?-2 This is the design part of this assignment. (3) Write the code for the above functions. You are NOT permitted to use SETF or DO in this code. You MUST use PURE LISP and recursion. If you do this you will find these functions are short. You MUST indent your code in a proper readable fashion. Learn to use == and =% in vi. When you apply a rewrite rule in dnf-distribute or dnf, you MUST call the LISP function RR to permit the rule to be traced. (4) Add tests to propositional-calculus.in for the EVALUATE function. (5) Test the code by running: make propositional-calculus.out and looking at the results. The theory part is worth 20 points, the design part 10 points, and the code part 30 points. Should you omit a function (or need to copy it from someone: be sure to comment that you have done so), points will be subtracted as follows: evaluate 8 theorem?-1 3 dnf-distribute 7 dnf 11 theorem?-2 1 These points happen to equal about half the number of lines of code containing a `)' in a well written version of the function (no, they need not add exactly to 30). Hints: (0) You can do this assignment one function at a time. START EARLY. Do the theory problems related to a function before you try to write the rewrite rules for the function, and do the rewrite rules before you write the function code. (1) The lecture on propositional calculus contains the basic information required to do the code part of this assignment. Reviewing the lecture on simple expressions and the associated code is also necessary. (2) We suggest you write the RR for a function first, then write the code, then test, all before going on to the next function. After you get the hang of it you can try several functions at once, but until you do, one function at a time is best. (3) EVALUATE. Given a constant, EVALUATE simply returns the constant. Given an operator with operands, EVALUATE calls itself to get values of the operands, and compares the results using EQL to 'T or 'F. Note: EVALUATE returns 'T or 'F: it does NOT return NIL, and you cannot use the result of EVALUATE directly as a COND test value. To evaluate (and e1 e2) first evaluate e1. Then if e1 evaluates to 'F, your are DONE: the final result is 'F. Otherwise the final result is the value of e2. OR is similar to AND but you are done if the value of e1 is 'T instead of 'F. (4) THEOREM?-1. Use the functions ONE-VARIABLE, EVALUATE, and ASSIGN. If the expression has no variables, evaluate it with EVALUATE. If the expression has a variable v, substitute T for that variable and see if the result is a theorem. If no, the original expression is not a theorem. If yes, then substitute F for v and see if that is a theorem. If yes, the original expression is a theorem; if no, it is not. (5) DNF-DISTRIBUTE. This just applies the distributive law to move AND inside OR, and does nothing else. Similar to APPLY-RULES from lecture, but much shorter. If you apply a rule, call (rr ...) to permit it to be traced. See NORMAL-2 from class for guidance on how this function is used. (6) DNF. If the expression is an AND or an OR, just apply DNF to its arguments and call DNF-DISTRIBUTE. If the expression is a NOT, apply NOT rules to move NOT inside other operators and get rid of double negation. The NOT rules are best applied in a dumb fashion: just apply them and run the result back through DNF. Do NOT try to normalize the operand of a NOT operator before applying a NOT rule. If you apply a NOT rule, call (rr ...) to permit it to be traced. See NORMAL-2 from class for guidance on how this function is used. These are the ONLY rules you need to apply. You do NOT need to sort AND or OR arguments or right associate them. (7) THEOREM?-2. This is a two-line function that uses DNF and UNSATISFIABLE-DNF get the result. See the lecture notes or book for the algorithm. Good Luck!