Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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