TD 6 : Herbrand, Compacité et Unification

EX 1

  • Entrée : une formule $𝜑$ sur ${\cal F, P}$, avec ${\cal F}$ réc. én.

Sans perte de généralité, on suppose $𝜑$ close

  • car si $𝜑$ non close :

    \[M \vDash 𝜑 ⟺ ∀𝜎, M, 𝜎 \vDash 𝜑\]

$𝜑$ valide

⟺ $∀M, M \vDash 𝜑$

⟺ $∀M, M \not\vDash ¬𝜑$

⟺ $\not ∃ M, M \vDash ¬𝜑$

⟺ $¬𝜑$ n’est pas satisfaisable

  1. $¬𝜑$ est logiquement équivalente à $𝜓$ où $𝜓$ est NNF (Non Negative Normal Form) (avec les règles de de Morgan).

  2. $𝜓’ = Sk(𝜓)$. Par le théorème de Skolem, $𝜓’$ est équisatisfaisable (mais PAS logiquement équivalente) à $𝜓$

    NB : Equivalence logique : tout modèle de l’une est modèle de l’autre VS Equisatisfaisabilité : pour tout modèle de l’une, il existe un modèle à l’autre

  3. On met $𝜓’$ sous forme prénexe : $𝜓’ = ∀x_1 ⋯ x_n 𝜑_0$, où $𝜑_0$ est sans quantificateurs

Théorème de Herbrand :

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

Application à $𝜓’$ : $𝜑$ valide ⟺ $𝜓’$ n’admet aucun modèle de Herbrand.

Modèle de Herbrand :

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

\[H(𝜑_0) = \lbrace 𝜑_0 𝜎 \mid 𝜎 : \lbrace x_1, ⋯, x_n \rbrace ⟶ T(F) \rbrace ⟺ H(𝜑_0) \text{ est insatisfaisable } \\ ⟺ \text{il existe un } H ⊆ H(𝜑_0) \text{ fini et insatisfaisable }\]

NB : le seul degré de liberté qu’on a dans un modèle de Herbrand est l’interprétation des prédicats. Donc à chaque valeur de prédicat (ex: $P(0,0)$), on associe une variable propositionnelle (on passe de $H’$ à $S_{H’}$), et on se ramène à la satisfiabilité dans la logique des propositions.

Pour un $H’$ fini, $H’$ satisfaisable ssi $S_{H’}$ est satisfaisable (calcul propositionnel).

Algo_valide(𝜑):

  Sk(¬𝜑) = ∀x_1, ⋯, x_n. 𝜓
  n = 0
  S = ∅
  n +=1 (L)
  S = S + {𝜓 𝜎 | 𝜎 n-ième substitution close}
  Si 𝜓 est insatisfiable: // en logique propositionnelle, où les termes clos sont les variables
    retourner Vrai
  Sinon:
    aller à (L)

OU

Algo_valide2(𝜑):

  S une partie non vide de H(𝜑_0)
  Pour chaque H':
    si S est insatisfiable :
      retourner "Valide"
    sinon:
        S = S + H'

NB : Pour “$S_{H’}$ est insatisfiable”, on peut procéder de deux manière :

  • il y a un nombre fini de variables, donc on peut tester toutes les valuations

  • OU : avec la complétude réfutationnelle de $Res+Fact$, cela revient à montrer $S_{H’} \vdash \bot$.

    Il suffit dont d’appliquer toutes les règles possibles depuis $S_{H’}$ : ça termine, et on trouve nécessairement $\bot$ si il y a insatisfaisabilité.

EX 2

\[P : x_1 = t_1 ∧ ⋯ ∧ x_n = t_n\]

$⟹$

Si $𝜎$ est un unificateur de $P$, montrons que $𝜎 = 𝜇𝜎$.

Il existe $𝜃$ unificateur tq

\[𝜎 = 𝜇𝜃 \\ ⟺ 𝜇𝜎 = 𝜇𝜇𝜃 = 𝜇𝜃 = 𝜎\]

(car le mgu $𝜇$ est idempotent)

$⟸$

Si $𝜎 = 𝜇𝜎$ :

Comme $𝜇$ est un unificateur :

\[∀i, x_i 𝜇 = 𝜏_i 𝜇 \\ ⟺ ∀i, x_i 𝜇 𝜎 = 𝜏_i 𝜇 𝜎 \\ ⟺ ∀i, x_i 𝜎 = 𝜏_i 𝜎\]

(par hypothèse)

EX 3

Supposons qu’il existe une telle $𝛹$, dont les modèles $M$ sont ceux tels que $D_M$ est infini.

On pose :

\[𝜑_k : "\text{il existe au moins k variables distinctes}"\]

i.e :

\[𝜑_k = ∃x_1, ⋯, x_k, \bigwedge\limits_{i≠j} ¬(x_i = x_j) \bigwedge{\cal T}_{=}\]

$S ≝ \lbrace ¬𝛹 \rbrace ∪ \lbrace 𝜓_n \rbrace_{n≥0}$ est satisfaisable ssi elle est finiment satisfaisable.

Or, $S$ est insatisfiable (car si $M \vDash S$, $M\vDash ¬𝛹$, donc $D_M$ est fini, ce qui contredit $M \vDash 𝜑_{\vert D_M \vert+1}$)

Donc il existe une partie finie $S’⊆S$ insatisfiable.

Or

  • $S’ ≝ \lbrace ¬𝛹 \rbrace ∪ \lbrace 𝜓_n \rbrace_{n≤k}$

  • OU $S’ ≝ \lbrace 𝜓_n \rbrace_{n≤k}$

dans les deux cas : en choisissant un modèle $M$ à $k+1$ élément, ce modèle satisfait $S’$ : absurde.

(exemple d’un tel modèle : un modèle de Herbrand à $k+1$ constantes où tous les prédicats sont interprétés par le vide et l’égalité par l’égalité numérique)

EX 5

$∀P∈𝒫, P⊆{\cal X}$.

Cas $F = ∅$ :

$𝜑$ satisfiable.

$𝒫$ fini.

Soit $M$ une $F, 𝒫$-strucutre tq

\[M\vDash 𝜑\] \[∀P∈𝒫, P_M ⊆ D_M\]

$∀x, y∈D_M$,

Soit $\sim$ définie par

\[x \sim y ⟺ (∀P, x∈P_M ⟺ y∈P_M)\]

$M’ = (D_M/\sim)$

Soit $P∈𝒫$.

\[D_M ≝ \lbrace [x] \mid x∈P_M \rbrace\]

Alors :

\[\vert D_{M'} \vert ≤ 2^{\vert 𝒫 \vert}\]

Mq

\[M' \vDash 𝜑\]

Hypothèse d’induction :

Pour toute sous-formule $𝜓$ de $𝜑$, pour toute $𝜎$ instantiation de $M$,

\[M,𝜎 \vDash 𝜓 ⟺ M', 𝜎' \vDash 𝜓\]

avec $𝜎’ = 𝜎/\sim$

Leave a comment