In this exercise, we will look at the recursive application of rewrite rules, using logic programming. A rewrite rule (or demodulator in OTTER terminology) is an equation with specified direction. For example, the rewrite rule x + O → x suggests replacing any expression that matches x + 0 with the expression x. The application of rewrite rules is a central part of educational reasoning systems. We will use the predicate rewrite (X, Y) to represent rewrite rules. For example, the earlier rewrite rule is written as rewrite (X + 0, X). Son terms arc primitive and cannot be further simplified thus, we will write primitive (0) say that 0 is a primitive term.

a. Write a definition of a predicate simplify (X, Y), that is true when Y is a simplified version of x—that is, when no further rewrite rules are applicable to any sub expression of Y.

b. Write a collection of rules for the simplification of expressions involving arithmetic operators, and apply your simplification algorithm to some sample expressions.

c. Write a collection of rewrite rules for symbolic differentiation, and use them along with your simplification rules to differentiate and simplify expressions involving arithmetic expressions including exponentiation.