Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:herbrand_s_expansion_theorem [2009/05/26 10:26] vkuncak |
sav08:herbrand_s_expansion_theorem [2009/05/26 10:28] vkuncak |
||
|---|---|---|---|
| Line 80: | Line 80: | ||
| This model induces an Herbrand model $(GT,\alpha_H)$, in which $\alpha_H(P)$ is a set of ground terms and $\alpha_H(R)$ is a relation on ground terms, $\alpha_H(R) \subseteq GT^2$. | This model induces an Herbrand model $(GT,\alpha_H)$, in which $\alpha_H(P)$ is a set of ground terms and $\alpha_H(R)$ is a relation on ground terms, $\alpha_H(R) \subseteq GT^2$. | ||
| - | To determine, for example, whether $(f(a,a),g(g(a))) \in \alpha_H(R)$ we check the truth value of the formula | + | To determine, for example, whether $(f(a,a),g(c)) \in \alpha_H(R)$ we check the truth value of the formula |
| \[ | \[ | ||
| R(f(a,a),g(c))) | R(f(a,a),g(c))) | ||
| \] | \] | ||
| - | in the original interpretation $(D,\alpha)$. In this case, the formula reduces to $1+1 < 2+1$ and is true in the interpretation. Therefore, we define $\alpha_H(R)$ to contain the pair of ground terms $(f(a,a),g(c)))$. | + | in the original interpretation $(D,\alpha)$. The truth value of the above formula in $\alpha$ reduces to $1+1 < 2+1$, which is true. Therefore, we define $\alpha_H(R)$ to contain the pair of ground terms $(f(a,a),g(c)))$. On the other hand, $R(f(a,a),c)$ evaluates to false in $(D,\alpha)$, so we define $\alpha_H(R)$ so that it does not contain the pair $(f(a,a),c)$. |