Question: 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 a 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 equational 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+O , X) . Some terms are primitive and cannot be further simplified; thus, we will write primitive ( 0 ) to 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 subexpression 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.