Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:ground_terms [2013/05/10 11:02] 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 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)$. | ||