Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:homework09 [2008/04/25 15:06]
vkuncak
sav08:homework09 [2015/04/21 17:30] (current)
Line 8: Line 8:
  
 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 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
-\[ +\begin{equation*} 
-    C \rightarrow \bigvee_{i=1} t_i=t'​_i +    C \rightarrow \bigvee_{i=1}^n t_i=t'​_i 
-\]+\end{equation*}
 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$ 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$
-\[+\begin{equation*}
     C \rightarrow t_i=t'​_i     C \rightarrow t_i=t'​_i
-\]+\end{equation*}
 holds for all values of variables in the Herbrand interpretation. 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. 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.
  
 
sav08/homework09.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice