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:ground_terms [2008/03/20 12:14] vkuncak |
sav08:ground_terms [2013/05/10 09:53] vkuncak |
||
---|---|---|---|
Line 9: | Line 9: | ||
i.e. built from constants using function symbols. | i.e. built from constants using function symbols. | ||
- | **Example** | + | **Example**\\ |
+ | ${\cal L}=\{a, f\}$ \\ | ||
+ | $GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$ | ||
If ${\cal L}$ has no constants then $GT$ is empty. In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$. We call the set $GT$ Herbrand Universe. | If ${\cal L}$ has no constants then $GT$ is empty. In that case, we add a fresh constant $a_0$ into the language and consider ${\cal L} \cup \{a_0\}$ that has a non-empty $GT$. We call the set $GT$ Herbrand Universe. | ||
Line 21: | Line 23: | ||
Let $ar(f)=n$. Then $f : GT^n \to GT$ | Let $ar(f)=n$. Then $f : GT^n \to GT$ | ||
- | $\alpha_H(f)(t_1,\ldots,t_n) =$ ++| $f(t_1,\ldots,t_n)$++ | + | $\alpha_H(f)(t_1,\ldots,t_n) = f(t_1,\ldots,t_n)$ |
- | This defines $\alpha_H(f)$. How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$? | + | This defines $\alpha_H(f)$. How to define $\alpha_H(R)$ to ensure that elements of a set are true, i.e. that $e_S(S)(I_H) = {\it true}$?\\ |
- | * is this possible for arbitrary set? | + | Partition $GT^n$ in two sets, one over which $\alpha_H(R)(t_1,...,t_n)$ is true and the other over which it is false. |
+ | * is this possible for arbitrary set? no | ||
**Example** | **Example** | ||
+ | Consider a set that is not satisfiable : $\{P(a),\ \neg P(a)\}$ | ||
===== Ground Atoms ===== | ===== Ground Atoms ===== | ||
Line 41: | Line 45: | ||
We will write $p(A)$. | We will write $p(A)$. | ||
- | **Example** | + | **Example**\\ |
- | + | ${\cal L}=\{a, f_1, P_1, R_2\}$ \\ | |
- | ===== Expansion of a Clause ===== | + | $GT=\{a, f(a), f(f(a)), f(f(f(a))), ...\}$\\ |
- | + | $HA=\{P(a), R(a,a), P(f(a)), R(a, f(a)), ...\}$\\ | |
- | Recall that we do not write quantifiers in the clause, but when we say that a clause is true in a model we mean that its universal closure is true. | + | $V=\{p_1, p_2, p_3, p_4, ...\}$\\ |
- | + | We define p such that :\\ | |
- | We obtain an instance of a clause $C$ by replacing all variables with some ground terms from $GT$. | + | $p(P(a))=p_1,\ p(R(a,a))=p_2,\ p(P(f(a)))=p_3,\ p(R(a, f(a)))=p_4,...$ |
- | + | ||
- | Define | + | |
- | \[ | + | |
- | expand(C) = \{ subst(\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\})(C) \mid FV(C) = \{x_1,\ldots,x_n\}\ \land\ t_1,\ldots,t_n \in GT \} | + | |
- | \] | + | |
- | + | ||
- | Note that if $C$ is true in $I$, then $expand(C)$ is also true in $I$ ($expand(C)$ is a consequence of $C$). | + | |
- | + | ||
- | We expand entire set: | + | |
- | \[ | + | |
- | expand(S) = \bigcup_{C \in S} expand(C) | + | |
- | \] | + | |
- | + | ||
- | Clauses in the expansion have no variables, they are //ground clauses//. | + | |
- | + | ||
- | ===== Constructing a Propositional Model ===== | + | |
- | + | ||
- | We can view the set $expand(S)$ as a set of propositional variables with "long names". | + | |
- | + | ||
- | For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$. | + | |
- | + | ||
- | **Example** | + | |
- | + | ||
- | Define propositional model $I_P : V \to \{{\it true},{\it false\}\}$ by | + | |
- | \[ | + | |
- | I_P(p(C_G)) = e_F(C_G)(I) | + | |
- | \] | + | |
- | + | ||
- | Let | + | |
- | \[ | + | |
- | propExpand(S) = \{ p(C_G) \mid C_G \in expand(S) \} | + | |
- | \] | + | |
- | + | ||
- | **Lemma:** If $I$ is a model of $S$, then $I_P$ is a model of $propExpand(S)$. | + | |
- | + | ||
- | Instead of searching for a model, we can search for a propositional model. | + | |
- | + | ||
- | If we prove there is no propositional model for $propExpand(S)$, then there is no model for $I$. | + | |
- | + | ||
- | What if there is a model $propExpand(S)$? Could it still be the case that $S$ is unsatisfiable? | + | |
- | + | ||
- | ===== 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$). | + | |
- | + | ||
- | We ensure that atomic formulas evaluate the same: | + | |
- | + | ||
- | $ \alpha_H(R) = \{ (t_1,\ldots,t_n)\ \mid $ ++| $I_P(p(R(t_1,\ldots,t_n))) \}$++ | + | |
- | + | ||
- | How does it evaluate non-ground formulas? | + | |
- | + | ||
- | **Lemma:** If $I_P$ is a model for $propExpand(S)$, then $(HU,\alpha_H)$ is a model for $S$. | + | |
- | + | ||
- | ===== Herbrand's Theorem ===== | + | |
- | + | ||
- | **Theorem:** The following statements are equivalent: | + | |
- | * set $S$ has a model | + | |
- | * set $propExpand(S)$ has a propositional model | + | |
- | * set $S$ has a model with domain $HU$ | + | |