• English only

# Differences

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

Link to this comparison view

sav08:ground_terms [2013/05/10 09:53]
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 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)$.

sav08/ground_terms.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice