Base di Herbrand

Da Wikipedia, l'enciclopedia libera.
Se riscontri problemi nella visualizzazione dei caratteri, clicca qui.

In logica matematica, per ogni linguaggio formale con un insieme di termini dall'universo di Herbrand, la base di Herbrand definisce ricorsivamente l'insieme di tutte le formule atomiche che possono essere composte formando predicati dai termini dell'universo di Herbrand. Una base di Herbrand di un linguaggio del primo ordine L può essere costruita dall'universo di Herbrand di L, applicando a ogni suo elemento qualche predicato di L. È dunque l'insieme di tutti gli atomi ground che possono essere costruiti usando simboli da L. Prende il nome da Jacques Herbrand. Nella base di Herbrand ogni elemento viene chiamato atomo.

Un’interpretazione su H(S) è completa per tutte le clausole di S quando ad ogni atomo della base si assegna un valore di verità.

La base di Herband è un insieme numerabile, i cui elementi possono essere ordinati. Per esempio, possono essere disposti in una successione ordinata \{P1,P2,...,Pn\}.

Termini e atomi di Herbrand[modifica | modifica sorgente]

Dato un linguaggio L(po), un termine di Herbrand è un termine base (ground term, ovvero un termine che non contiene variabili)

Esempi: f(a), g(a,b), g(f(a),b), g(f(a),g(b,c)), g(f(a),g(f(b),c)),...

Un atomo di Herbrand è un atomo base (ground atom, ovvero un atomo che non contiene variabili)

Esempi: P(f(a)), P(g(a,b)), Q(g(f(a),b), g(f(a),g(b,c))), ...

Universo e base di Herbrand[modifica | modifica sorgente]

L’universo di Herbrand è l’insieme di tutti i termini di Herbrand. Esempio:  U(H)= \{a, b, c, f(a), g(a,b), g(f(a),b), g(f(a),g(b,c)), g(f(a),g(f(b),c)),\dots\}

La base di Herbrand è l’insieme di tutti gli atomi di Herbrand. Esempio: B(H)= \{P(a), P(b), P(c), P(f(a)), P(g(a,b)), Q(g(f(a),b), g(f(a),g(b,c))),\dots\}

Sistemi di Herbrand[modifica | modifica sorgente]

Sistema di Herbrand di un enunciato universale Dato un enunciato universale, della forma \forall x_1 \forall x_2 \dots \forall x_n \varphi (\varphi non contiene quantificatori).

Il Sistema di Herbrand è l’insieme (anche infinito) di formule chiuse generato per sostituzione \varphi [x_1/t_1, x_2/t_2, \dots, x_n/t_n] con tutte le possibili combinazioni <t_1,t_2,...,t_n> di t(i) appartenente a U(H). Esempi:


H(\forall x P(x)\in Q(x))) = \{P(f(a))\in Q(f(a)), P(g(a,b))\in Q(g(a,b)),...\} \,\!

H(\forall x \forall y R(x,y)) = \{R(f(a), f(a)), R(g(a,b), f(a)), R(f(a), g(a,b)),...\} \,\!

Sistema di Herbrand di una teoria[modifica | modifica sorgente]

Data una teoria \sum di enunciati universali è[Cosa?] l’unione H(\sum) di tutti i sistemi di Herbrand generati dagli enunciati \sum.

Esempio:


\sum= \{ \varphi, \psi, X\}

H\left(\sum\right)=H(\varphi) \bigcup H(\psi) \bigcup H(X)

Teorema di Herbrand[modifica | modifica sorgente]

Data una teoria di enunciati universali \sum, H(\sum) ha un modello se e solo se \sum ha un modello; questa caratteristica è utile in quanto H(\sum) può essere infinito anche quando \sum è finito. Il teorema si applica solo agli enunciati universali.

Corollario (forma a clausole di Horn)[modifica | modifica sorgente]

Sia \tau un insieme di clausole di Horn, le seguenti affermazioni sono equivalenti:

  • \tau è soddisfacibile.
  • \tau ha un modello di Herbrand.

È da notare che si afferma che \tau ha un modello di Herbrand, non H(\tau). Non vale in generale: solo se \tau è un insieme clausole di Horn. In questa forma (finita), è quasi una procedura effettiva.

Bibliografia[modifica | modifica sorgente]

Voci correlate[modifica | modifica sorgente]

matematica Portale Matematica: accedi alle voci di Wikipedia che trattano di matematica