Lab for Automated Reasoning and Analysis LARA

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