# Homework 09 - Due Wednesday, April 30

## Problem 1

Describe current progress on your project.

## Problem 2

Prove that the quantifier-free theory of term algebras is convex (See Calculus of Computation Textbook, Section 10.3.1). That is, show that, if is a conjunction of literals of form and where are terms in some language (containing variables), and if formula

is valid (holds for all values of variables) in the Herbrand interpretation (where elements are ground terms and ), then for some

holds for all values of variables in the Herbrand interpretation.

If you use in your solution any theorem about term algebras that we did not prove in the class, you need to prove the theorem as well.