This is an old revision of the document!

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 $C$ is a conjunction of literals of form $t=t'$ and $t\neq t'$ where $t,t'$ are terms in some language (containing variables), and if formula \[

  C \rightarrow \bigvee_{i=1} t_i=t'_i

\] is valid (holds for all values of variables) in the Herbrand interpretation (where elements are ground terms and $\alpha(f)(t_1,\ldots,t_n)=f(t_1,\ldots,t_n)$ ), then for some $i$ \[

  C \rightarrow t_i=t'_i

\] holds for all values of variables in the Herbrand interpretation.