This is an old revision of the document!
Homework 09 - DRAFT, 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 \[
C \rightarrow \bigvee_{i=1} t_i=t'_i
\] is valid (holds for all values of variables) in the Herbrand interpretation, then for some \[
C \rightarrow t_i=t'_i
\] holds for all values of variables.