Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:herbrand_s_expansion_theorem [2008/03/24 11:32] vkuncak |
sav08:herbrand_s_expansion_theorem [2009/05/26 10:26] vkuncak |
||
|---|---|---|---|
| Line 23: | Line 23: | ||
| ===== Constructing a Propositional Model ===== | ===== Constructing a Propositional Model ===== | ||
| - | We can view the set $expand(S)$ as a set of propositional variables with "long names". | + | We can view the set $expand(S)$ as a set of propositional formulas whose propositional variables have "long names". |
| For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$. | For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$. | ||
| **Example** | **Example** | ||
| + | Let's consider the expanded formula $F=P(f(a)) \wedge R(a, f(a))$, then $p(F)=p_1 \wedge p_4$ | ||
| - | Define propositional model $I_P : V \to \{{\it true},{\it false\}\}$ by | + | Define propositional model $I_P : V \to \{\it true},{\it false\}$ by |
| \[ | \[ | ||
| I_P(p(C_G)) = e_F(C_G)(I) | I_P(p(C_G)) = e_F(C_G)(I) | ||
| Line 65: | Line 66: | ||
| * set $propExpand(S)$ has a propositional model | * set $propExpand(S)$ has a propositional model | ||
| * set $S$ has a model with domain $GT$ | * set $S$ has a model with domain $GT$ | ||
| + | |||
| + | **Example:** Take the first three clauses our example (from [[Normal Forms for First-Order Logic]]): | ||
| + | * $R(x,g(x))$ | ||
| + | * $\neg R(x,y) \lor R(x,f(y,z)))$ | ||
| + | * $P(x) \lor P(f(x,a))$ | ||
| + | Taking as domain $D$ the set of natural numbers, the structure $(D,\alpha)$ is a model of the conjunction of these three clauses, where $\alpha$ is given by: | ||
| + | * $\alpha(a) = 1$ | ||
| + | * $\alpha(c) = 2$ | ||
| + | * $\alpha(g)(x) = (x + 1)$ | ||
| + | * $\alpha(f)(y,z) = y+z$ | ||
| + | * $\alpha(R) = \{(x,y).\ x < y\}$ | ||
| + | * $\alpha(P) = \{x.\ x \mbox{ is even} \}$ | ||
| + | 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 | ||
| + | \[ | ||
| + | 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)))$. | ||