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:24] vkuncak |
sav08:herbrand_s_expansion_theorem [2008/04/01 15:59] giuliano |
||
|---|---|---|---|
| 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 49: | Line 50: | ||
| ===== Constructing Herbrand Model ===== | ===== Constructing Herbrand Model ===== | ||
| - | For $I = (HU,\alpha_H)$ we define $\alpha_H(R)$ so that $I_H$ evaluates ground formulas $expand(S)$ same as in $I_P$ (and thus same as in $I$). | + | For $I = (GT,\alpha_H)$ we define $\alpha_H(R)$ so that $I_H$ evaluates ground formulas $expand(S)$ same as in $I_P$ (and thus same as in $I$). |
| We ensure that atomic formulas evaluate the same: | We ensure that atomic formulas evaluate the same: | ||