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 (where elements are ground terms and ), then for some
\[
C \rightarrow t_i=t'_i
\] holds for all values of variables in the Herbrand interpretation.