TD 7 : Herbrand & Prolog

EX 2

Modèle de Herbrand :

une $F, P$-structure $H$ sur la $F$-algèbre $T(F)$ (termes clos).

Soient $H_1, H_2$ des modèles de Herbrand d’un ensemble $S$ de clauses de Horn, i.e des clauses ayant au plus un atome (prédicat appliqué à des termes) positif.

Montrons que $H_1 ∩ H_2$ reste un modèle de $S$

NB : le seul degré degré de liberté qu’on a pour les modèles de Herbrand est l’interprétation des prédicats (le domaine est fixé par la $F$-algèbre : les termes clos). Donc l’intersection est l’intersection des interprétations des prédicats.

Il suffira de montrer que si $C$ est une clause de Horn :

H_1 \vDash C \text{ et } H_2 \vDash C ⟹ H_1 ∩ H_2 \vDash C

NB : $C$ est de la forme :

C ≝ ∀\, \overline{x}. \, (A ∨ ¬ B_1 ∨ ⋯ ∨ ¬ B_n)

  • $n≥0$
  • $A = P(t_1, ⋯, t_r)$ pour des termes $t_i$
  • $B_i = P_i(t^i_1, ⋯, t^i_s)$ pour des termes $t’_j$

Soit $𝜎$ une instantiation de $H_1 ∩ H_2$.

Montrons que

H_1 ∩ H_2, 𝜎 \vDash C

i.e

H_1 ∩ H_2, 𝜎 \vDash A \text{ ou il existe } i \text{ tq } H_1 ∩ H_2, 𝜎 \vDash B_i

Comme $H_1, 𝜎 \vDash C$ et $H_2, 𝜎 \vDash C$ :

H_1, 𝜎 \vDash A \text{ ou il existe } i \text{ tq } H_1, 𝜎 \vDash ¬ B_i

et

H_2, 𝜎 \vDash A \text{ ou il existe } j \text{ tq } H_2, 𝜎 \vDash ¬ B_j
  • Soit $H_1, 𝜎 \vDash A$ et $H_2, 𝜎 \vDash A$, auquel cas on conclut

  • Soit il existe (sans perte de généralité) $i$ tel que $H_1, 𝜎 \vDash ¬B_i$, *i.e* $\overline{t^i}𝜎 ∉ {P_i}_{H_1}$, donc en particulier $\overline{t^i}𝜎 ∉ {P_i}_{H_1}∩{P_i}_{H_1}$

3.

T_P(H) ≝ H ∪ \lbrace A𝜎∈Atomes clos \mid ∃ A∨¬B_1∨⋯ ∨¬B_n∈P \rbrace

où $H⊆\text{Atomes clos}$ tq $B_1 𝜎, ⋯, B_n 𝜎∈H$

$T_P$ : opérateur de conséquence immédiate.

$H \vDash P$ ssi $T_P(H)=H$

M_P ≝ \bigcup\limits_{n≥0} T_P^n(∅)

Mq

P \vDash R ⟺ M_P \vDash R

$⟹$ :

Supposons que $P \vDash R$.

Comme $M_P = T_P(M_P)$ et $P$ est un programme, $M_P \vDash P$, $M_P \vDash R$.

$⟸$ :

Supposons que $M_P \vDash R ≝ ∃ \overline{x}. (A_1 ∧ ⋯ ∧ A_n)$.

Montrons que $P \vDash R$, i.e $P ∪ ¬ R \vDash \bot$.

C’est-à-dire, d’après le théorème de Herbrand (puisque $P ∪ ¬ R$ est un ensemble de formules universellement quantifiées), que $P ∪ ¬ R$ n’a pas de modèle de Herbrand.

Th de Herbrand :

pour toute formule close $𝜑$ universellement quantifiée, $𝜑$ est satisfiable ssi elle a un modèle de Herbrand.

Par l’absurde : supposons qu’il existe une modèle de Herbrand $M$ tel que

M \vDash P ∪ ¬ R

donc

M \vDash ¬ R

et comme $M_P ⊆ M$ ($M$ est un point fixe de $T_P$ car $M \vDash P$)

M_P \vDash ¬ R
  • car pour tout $𝜎 : X ⟶ T(F)$, $M, 𝜎 \vDash ¬ A_1(\overline{t_1}) ∨ ⋯ ∨ ¬ A_n(\overline{t_n})$, d’où $∃i$ tq \overline{t_i}𝜎 ∉ {P_i}_{M}, d’où \overline{t_i}𝜎 ∉ {P_i}_{M_P}, et $M_P \vDash ¬ R$

ce qui est absurde, puisque $M_P \vDash R$.

5.

1.

Supposons que

M \vDash 𝜓 ≝ ∃x_1, \ldots, x_n, ∀ y_1, \ldots, y_k

(à finir pour la prochaine fois)

Leave a comment