• English only

# Differences

This shows you the differences between two versions of the page.

 sav08:ground_terms [2013/05/10 09:53]vkuncak sav08:ground_terms [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2013/05/10 11:02 vkuncak 2013/05/10 09:53 vkuncak 2009/05/13 10:29 vkuncak 2008/04/01 15:55 giuliano 2008/04/01 15:29 giuliano 2008/04/01 15:26 giuliano 2008/03/28 17:35 giuliano 2008/03/20 12:15 vkuncak 2008/03/20 12:14 vkuncak 2008/03/20 12:13 vkuncak 2008/03/20 12:03 vkuncak 2008/03/20 12:02 vkuncak 2008/03/20 12:00 vkuncak 2008/03/20 11:57 vkuncak 2008/03/20 11:57 vkuncak 2008/03/20 11:33 vkuncak 2008/03/20 11:32 vkuncak 2008/03/20 11:17 vkuncak 2008/03/20 11:16 vkuncak 2008/03/20 11:04 vkuncak 2008/03/20 11:04 vkuncak 2008/03/20 11:03 vkuncak 2008/03/20 10:48 vkuncak created Next revision Previous revision 2013/05/10 11:02 vkuncak 2013/05/10 09:53 vkuncak 2009/05/13 10:29 vkuncak 2008/04/01 15:55 giuliano 2008/04/01 15:29 giuliano 2008/04/01 15:26 giuliano 2008/03/28 17:35 giuliano 2008/03/20 12:15 vkuncak 2008/03/20 12:14 vkuncak 2008/03/20 12:13 vkuncak 2008/03/20 12:03 vkuncak 2008/03/20 12:02 vkuncak 2008/03/20 12:00 vkuncak 2008/03/20 11:57 vkuncak 2008/03/20 11:57 vkuncak 2008/03/20 11:33 vkuncak 2008/03/20 11:32 vkuncak 2008/03/20 11:17 vkuncak 2008/03/20 11:16 vkuncak 2008/03/20 11:04 vkuncak 2008/03/20 11:04 vkuncak 2008/03/20 11:03 vkuncak 2008/03/20 10:48 vkuncak created 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 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)$.