Espressione ground

Termine ground

Un termine ground è un termine che non contiene variabili.

I termini ground possono essere definiti ricorsivamente come segue:

1. Gli elementi di ${\displaystyle C}$ sono termini ground;
2. Se ${\displaystyle f\in F}$ è il simbolo di una funzione ${\displaystyle n}$-aria e ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$ sono termini ground, allora ${\displaystyle f\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$ è un termine ground.
3. Ogni termine ground può essere generato applicando le due regole di cui sopra.

In altre parole, l'universo di Herbrand è l'insieme di tutti i termini ground.

Atomo ground

Un atomo ground (o predicato ground) è una formula atomica in cui tutti i termini sono ground.

Se ${\displaystyle p\in P}$ è il simbolo di un predicato ${\displaystyle n}$-ario e ${\displaystyle \alpha _{1},\alpha _{2},\ldots ,\alpha _{n}}$ sono termini ground, allora ${\displaystyle p\left(\alpha _{1},\alpha _{2},\ldots ,\alpha _{n}\right)}$ è un atomo ground.

In altre parole, la base di Herbrand è l'insieme di tutti gli atomi ground. Invece, l'interpretazione di Herbrand assegna un valore di verità ad ogni atomo ground nella base.

Formula ground

Una formula ground è una formula senza variabili.

Le formule senza variabili possono essere definite ricorsivamente come segue:

1. Un atomo ground è una formula ground.
2. Se ${\displaystyle \varphi }$ e ${\displaystyle \psi }$ sono formule ground, allora ${\displaystyle \lnot \varphi }$, ${\displaystyle \varphi \lor \psi }$ e ${\displaystyle \varphi \land \psi }$ sono formule ground.

Le formule ground sono un particolare tipo di formule chiuse.