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)\]

où

• $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)