Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:ground_terms [2009/05/13 10:29] vkuncak |
sav08:ground_terms [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| //Ground term// is a term $t$ without variables, i.e. $FV(t)=\emptyset$, i.e. given by grammar: | //Ground term// is a term $t$ without variables, i.e. $FV(t)=\emptyset$, i.e. given by grammar: | ||
| - | \[ | + | \begin{equation*} |
| GT ::= f(GT,\ldots,GT) | GT ::= f(GT,\ldots,GT) | ||
| - | \] | + | \end{equation*} |
| i.e. built from constants using function symbols. | i.e. built from constants using function symbols. | ||
| Line 15: | Line 15: | ||
| 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. | ||
| - | Goal: show that if a formula //without equality// (for now) has a model, then it has a model whose domain is Herbrand universe, that is, a model of the form $I_H = (HU,\alpha_H)$. | + | Goal: show that if a formula //without equality// (for now) has a model, then it has a model whose domain is Herbrand universe, that is, a model of the form $I_H = (GT,\alpha_H)$. |
| How to define $\alpha_H$? | How to define $\alpha_H$? | ||
| Line 23: | 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}$?\\ | ||
| 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. | 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 ++ | + | * is this possible for arbitrary set? no |
| **Example** | **Example** | ||
| Line 35: | Line 35: | ||
| If $R \in {\cal L}$, $ar(R)=n$ and $t_1,\ldots,t_n \in GT$, we call $R(t_1,\ldots,t_n)$ an Herbrand Atom. HA is the set of all Herbrand atoms: | If $R \in {\cal L}$, $ar(R)=n$ and $t_1,\ldots,t_n \in GT$, we call $R(t_1,\ldots,t_n)$ an Herbrand Atom. HA is the set of all Herbrand atoms: | ||
| - | \[ | + | \begin{equation*} |
| HA = \{ R(t_1,\ldots,t_n) \mid R \in {\cal L}\ \land \ t_1,\ldots,t_n \in GT \} | HA = \{ R(t_1,\ldots,t_n) \mid R \in {\cal L}\ \land \ t_1,\ldots,t_n \in GT \} | ||
| - | \] | + | \end{equation*} |
| We order elements of $HA$ in sequence (e.g. sorted by length) and establish a bijection $p$ with propositional variables | We order elements of $HA$ in sequence (e.g. sorted by length) and establish a bijection $p$ with propositional variables | ||
| - | \[ | + | \begin{equation*} |
| p : HA \to V | p : HA \to V | ||
| - | \] | + | \end{equation*} |
| We will write $p(A)$. | We will write $p(A)$. | ||