DM : QBF et la logique intuitionniste

2 minute read

DM de Logique 2 : Procédure de décision par résolution pour les logiques de description.

Younesse Kaddar

I. Résolution étiquetée

NB :

  • Si ${\cal E}$ est un ensemble de clauses et $C$ une clause, on note ${\cal E} \vdash_{S_e} C$ le fait qu’il existe une preuve de $C$ à partir de ${\cal E}$.

  • On note $\vdash_R$ (resp. $\vdash_F$) la relation de déduction associée à la règle $R$ (resp. $F$).

Question 1.1

  1. Remarquons déjà que comme les clauses sont supposées sans variables, pour toute substitution close $𝜎$ :
\[C 𝜎 = C\] 
(Ce qui concerne les unificateurs dans les deux règles d'inférence de $S_e$ peut donc être ignoré dans cette première question)

  1. Par commodité d’écriture, on réécrit la règle $(F)$ sous la forme :

    \[\cfrac{L:e ∨ L':e' ∨ C \qquad L:e ∨ L':e' ∨ C}{ (L:e ∨ C)𝜎} \; (F) \quad \text{ si } \quad \begin{cases} 𝜎 = \textsf{mgu}(L, L') \\ L':e' ∈ s(L:e ∨ L':e' ∨ C) \end{cases}\]

    pour avoir des arbres de preuves binaires.

    Cela ne pose pas de problème, dans la mesure où on considère des ensembles de clauses, et non pas des multi-ensembles (les clauses ne sont pas comptées avec multiplicité, donc dupliquer une hypothèse n’a que des conséquences syntaxiques (sur la forme des arbres de preuves)).

Supposons que $\bot ∉ {\cal E}^\ast$, $C ≝ L:e ∨ C’$ est une clause minimale de ${\cal E}^\ast$ et $L$ est un littéral maximal de $C ≝ L:e ∨ C’$.

Par l’absurde : si $\bot ∈ ({\cal E}^\ast(L))^\ast$, i.e ${\cal E}^\ast(L) \vdash_{S_e} \bot$ :

  • Cas 1 : $\bot∈{\cal E}^\ast(L)$

    alors, par définition de ${\cal E}^\ast(L)$ :

    • Sous-Cas 1 : $\bot ∈ {\cal E}^\ast$ : ce cas est exclus, par hypothèse.

    • Sous-Cas 2 : $\bot ∨ \overline{L}:e’ = \overline{L}:e’ ∈ {\cal E}^\ast$ :

      alors par maximalité de $L$ dans $C$ :

      \[C, \overline{L} \vdash_R C'\]

      et $C’∈{\cal E}^\ast$, ce qui contredit la minimalité de $C$

  • Cas 2 : il existe un arbre de preuve (non réduit à sa racine) de la forme

    \[\cfrac{\cfrac{ \cfrac{\cfrac{\vdots}{C^1_{n-2}} \; (I^1_{n-3}) \qquad \cfrac{\vdots}{C'^1_{n-2}} \; (I^2_{n-3})}{C^1_{n-1}} \; (I^1_{n-2}) \qquad \cfrac{ \cfrac{\vdots}{C^2_{n-2} } \; (I^3_{n-3}) \qquad \cfrac{\vdots}{C'^2_{n-2}} \; (I^4_{n-3})}{C^1_{n-1}} \; (I^2_{n-2})}{C^1_n} \; (I^1_{n-1}) \qquad \cfrac{\cfrac{ \cfrac{\vdots}{C^3_{n-2} } \; (I^5_{n-3}) \qquad \cfrac{\vdots}{C'^3_{n-2}} \; (I^6_{n-3})}{C^2_{n-1}} \; (I^3_{n-2}) \qquad \cfrac{ \cfrac{\vdots}{C^4_{n-2}} \; (I^7_{n-3}) \qquad \cfrac{\vdots}{C'^4_{n-2}} \; (I^8_{n-3})}{C'^2_{n-1}} \; (I^4_{n-2})}{C'^1_n} \; (I^2_{n-1})}{\bot} \; (I^1_n)\] 
        digraph {
      rankdir=TB;
      C_n, "C'_n" -> ⊥[label="   I_n"];
      C_nn, "C'_nn" -> C_n[label="   I_n"];
    }

Leave a comment