TP 11 : Preuve automatique en déduction naturelle

Solution

open Dnat

let seq gamma phi = {gamma; phi}

(* Réponse Q1 *)
let rec string_of_formule = function
  | Var v -> v
  | Bot -> "F"
  | And (f1, f2) -> "(" ^ string_of_formule f1 ^ " & " ^ string_of_formule f2 ^ ")"
  | Or (f1, f2) -> "(" ^ string_of_formule f1 ^ " | " ^ string_of_formule f2 ^ ")"
  | Implies (f1, f2) -> "(" ^ string_of_formule f1 ^ " -> " ^ string_of_formule f2 ^ ")"
  | Not f -> "(! " ^ string_of_formule f ^ ")"


(* Réponse Q2 *)
let string_of_sequent s =
  let gamma_str = String.concat ", " (List.map string_of_formule s.gamma) in
  gamma_str ^ " |- " ^ string_of_formule s.phi

(* Réponse Q3 *)
let appliquer_regle r s =
  match r, s.phi with
  | Axiom, _ ->
      if List.mem s.phi s.gamma then Some [] else None
  | AndIntro, And (f1, f2) ->
      Some [seq s.gamma f1; seq s.gamma f2]
  | OrIntro1, Or (f1, _) ->
      Some [seq s.gamma f1]
  | OrIntro2, Or (_, f2) ->
      Some [seq s.gamma f2]
  | ImpliesIntro, Implies (f1, f2) ->
      Some [seq (f1 :: s.gamma) f2]
  | NotIntro, Not f ->
      Some [seq (f :: s.gamma) Bot]
  | ImpliesElim f1, _ ->
      Some [seq s.gamma (Implies (f1, s.phi)); seq s.gamma f1]
  | AndElim1 f2, _ ->
      Some [seq s.gamma (And (s.phi, f2))]
  | AndElim2 f1, _ ->
      Some [seq s.gamma (And (f1, s.phi))]
  | NotElim f, Bot ->
      Some [seq s.gamma (Not f); seq s.gamma f]
  | OrElim (f1, f2), _ ->
      (* Pour prouver phi par OrElim, il faut prouver qu'on a f1 \/ f2, puis que f1 implique phi, et f2 implique phi *)
      Some [
        seq s.gamma (Or (f1, f2));
        seq (f1 :: s.gamma) s.phi;
        seq (f2 :: s.gamma) s.phi
      ]
  | _, _ -> None

(* Fonction utilitaire : Extraire les sous-formules *)
(* Réponse Q4 *)
let rec sous_formules_f f =
  match f with
  | And (f1, f2) | Or (f1, f2) | Implies (f1, f2) ->
      f :: (sous_formules_f f1 @ sous_formules_f f2)
  | Not f1 -> f :: sous_formules_f f1
  | _ -> [f]

(* Réponse Q5 *)
let sous_formules_gamma gamma = List.map sous_formules_f gamma |> List.concat

(* Réponse Q6 *)
let regles_possibles s =
  let intros = match s.phi with
    | And _ -> [AndIntro]
    | Or _ -> [OrIntro1; OrIntro2]
    | Implies _ -> [ImpliesIntro]
    | Not _ -> [NotIntro]
    | _ -> []
  in
  let elims = 
    let sf = sous_formules_gamma s.gamma in
    let list_elims_classiques = List.concat (List.map (fun f -> [AndElim1 f; AndElim2 f; ImpliesElim f; NotElim f]) sf) in
    let list_or_elims = 
      List.filter_map (fun f -> 
        match f with
        | Or (f1, f2) -> Some (OrElim (f1, f2))
        | _ -> None
      ) sf
    in
    list_elims_classiques @ list_or_elims
  in
  (* On privilégie l'axiome, puis les intros, puis les éliminations limitées aux sous-formules *)
  Axiom :: (intros @ elims)

(* Réponse Q7 *)
let rec prouver depth s =
  if depth <= 0 then None
  else
    let rules = regles_possibles s in
    let rec try_rules = function
      | [] -> None
      | r :: rs ->
          match appliquer_regle r s with
          | None -> try_rules rs
          | Some premises ->
              let rec prove_all = function
                | [] -> Some []
                | p :: ps ->
                    match prouver (depth - 1) p with
                    | None -> None
                    | Some tree ->
                        match prove_all ps with
                        | None -> None
                        | Some trees -> Some (tree :: trees)
              in
              match prove_all premises with
              | None -> try_rules rs
              | Some trees -> Some (Noeud (r, s, trees))
          in try_rules rules

(* Réponse Q8 *)
let prouver_min max_depth s =
  let rec iter depth =
    if depth > max_depth then None
    else match prouver depth s with
      | Some arbre -> Some arbre
      | None -> iter (depth + 1)
  in iter 1

let tests = [
  "|- A -> A";
  "|- (A & B) -> (B & A)";
  "|- A -> (B -> A)";
  "|- ((A -> B) & A) -> B";
  "|- (A & (B | C)) -> ((A & B) | (A & C))";
  "|- (A & !A) -> F";
]

let run_test seq_str =
  let seq = parse seq_str in
  Printf.printf "\nTest : %s\n" (string_of_sequent seq);
  match prouver_min 8 seq with
  | None -> Printf.printf "  -> Echec de la preuve\n"
  | Some arbre ->
      Printf.printf "  -> Succes !\n";
      afficher_arbre_preuve arbre

let () =
  List.iter run_test tests

Dans ce TP, nous implémentons un prouveur de théorèmes pour la logique minimale en déduction naturelle.

Représentation

0. Télécharger dnat.ml qui définit les types ci-dessous et écrire une fonction utilitaire seq : formule list -> formule -> sequent renvoyant un séquent $\Gamma\vdash\varphi$ à partir de $\Gamma$ et $\varphi$.

type formule =
  | Var of string
  | Bot
  | And of formule * formule
  | Or of formule * formule
  | Implies of formule * formule
  | Not of formule

type sequent = {
  gamma : formule list;
  phi : formule;
}

On utilisera les types et fonctions de dnat.ml avec open Dnat au début de votre fichier.

Compilation : ocamlc dnat.ml tp.ml && ./a.out.

On utilisera aussi utop pour les tests, en exécutant #mod_use "chemin/vers/dnat.ml";; dans utop.

1. Écrire une fonction string_of_formule : formule -> string avec F, &, |, ! pour faux, et, ou, non.
   On rappelle que ^ sert à concaténer des chaînes en OCaml.
2. Écrire une fonction string_of_sequent : sequent -> string.

string_of_formule (And (Var "A", Not (Var "B"))) (* "(A & (! B))" *)
string_of_formule (Implies (Var "A", Or (Var "A", Var "B"))) (* "(A -> (A | B))" *)

string_of_sequent { gamma = [Var "A"; Implies (Var "A", Var "B")]; phi = Var "B" } (* "A, (A -> B) |- B" *)

Règles et arbres de preuve

Les types suivants sont définis dans dnat.ml :

type regle =
  | Axiom
  | ImpliesIntro | ImpliesElim of formule
  | AndIntro | AndElim1 of formule | AndElim2 of formule
  | OrIntro1 | OrIntro2 | OrElim of formule * formule
  | NotElim of formule | NotIntro

type arbre_preuve = Noeud of regle * sequent * arbre_preuve list

Par exemple, ImpliesElim (And (Var "A", Var "B")) correspond à appliquer la règle d'élimination de l'implication où $X$ est remplacé par $A \land B$.

	Axiome	Implication	Conjonction	Disjonction	Negation
Intro
Elim

3. Écrire appliquer_regle : regle -> sequent -> sequent list option vérifiant si la règle est applicable au séquent donné, et si oui, renvoyant la liste des prémisses à prouver. Si la règle n'est pas applicable, renvoyer None. Pour simplifier, on utilise ci-dessous la fonction parse : string -> sequent de dnat.ml pour construire les séquents.

appliquer_regle Axiom (parse "A |- A");;
- : sequent list option = Some []
appliquer_regle Axiom (parse "A |- B");;
- : sequent list option = None
appliquer_regle AndIntro (parse "A |- (A & B)");;
- : sequent list option =
Some [{gamma = [Var "A"]; phi = Var "A"}; {gamma = [Var "A"]; phi = Var "B"}]
appliquer_regle (NotElim ((parse "A | B").phi)) (parse "B, !A |- F");;
- : sequent list option =
Some
 [{gamma = [Var "B"; Not (Var "A")]; phi = Not (Or (Var "A", Var "B"))};
  {gamma = [Var "B"; Not (Var "A")]; phi = Or (Var "A", Var "B")}]
appliquer_regle (OrElim (Var "A", Var "B")) (parse "|- C");;
- : sequent list option =
Some
 [{gamma = []; phi = Or (Var "A", Var "B")};
  {gamma = [Var "A"]; phi = Var "C"}; {gamma = [Var "B"]; phi = Var "C"}]

Recherche de preuve

4. Écrire sous_formules_f : formule -> formule list qui renvoie la liste de toutes les sous-formules d'une formule donnée (y compris la formule elle-même).

sous_formules_f (parse "A & (B | C)").phi;;
- : formule list =
[And (Var "A", Or (Var "B", Var "C")); Var "A"; Or (Var "B", Var "C");
 Var "B"; Var "C"]

5. Écrire sous_formules_gamma : formule list -> formule list qui renvoie la liste de toutes les sous-formules présentes dans le contexte gamma.

sous_formules_gamma (parse "(A & B), (C | D) |- A").gamma;;
- : formule list =
[And (Var "A", Var "B"); Var "A"; Var "B"; Or (Var "C", Var "D"); Var "C";
 Var "D"]

6. Écrire regles_possibles : sequent -> regle list qui, étant donné un séquent, renvoie la liste des règles de déduction naturelle applicables pour prouver ce séquent. On utilisera les sous-formules du contexte $\Gamma$ pour limiter les règles proposées.

Ainsi, sur un séquent $\Gamma \vdash A$ :

• Ajouter les règles d'introductions qui permettent d'obtenir $A$ (exemple : AndIntro si $A$ est de la forme $B \land C$).
• Ajouter les règles d'élimination qui permettent d'obtenir $A$ à partir de n'importe quelles sous-formules présentes dans $\Gamma$. On appliquera OrElim (X, Y) seulement si $\Gamma$ contient $X\lor Y$ comme sous-formule.

regles_possibles (parse "(A & B) |- A");;
- : regle list =
[Axiom; AndElim1 (And (Var "A", Var "B")); AndElim2 (And (Var "A", Var "B"));
 ImpliesElim (And (Var "A", Var "B")); NotElim (And (Var "A", Var "B"));
 AndElim1 (Var "A"); AndElim2 (Var "A"); ImpliesElim (Var "A");
 NotElim (Var "A"); AndElim1 (Var "B"); AndElim2 (Var "B");
 ImpliesElim (Var "B"); NotElim (Var "B")]

7. Écrire prouver : int -> sequent -> arbre_preuve option qui, étant donné une profondeur maximale depth et un séquent, renvoie un arbre de preuve pour ce séquent. On utilisera afficher_arbre_preuve : arbre_preuve -> unit de dnat.ml pour afficher l'arbre de preuve.

Indications :

• Cas de base : si depth <= 0, renvoyer None.
• Sinon, essayer les règles retournées par regles_possibles une par une.
• Pour une règle applicable, prouver toutes les prémisses avec profondeur depth - 1.
• Si une prémisse échoue, revenir en arrière (backtracking) et tester la règle suivante.

prouver 2 (parse "(A & B) |- A") |> Option.iter afficher_arbre_preuve
  [AndElim1(B)] (A & B) |- A
    [Axiom] (A & B) |- (A & B)
prouver 4 (parse "|- (A & B) -> (B & A)") |> Option.iter afficher_arbre_preuve
  [ImpliesIntro]  |- ((A & B) -> (B & A))
    [AndIntro] (A & B) |- (B & A)
      [AndElim2(A)] (A & B) |- B
        [Axiom] (A & B) |- (A & B)
      [AndElim1(B)] (A & B) |- A
        [Axiom] (A & B) |- (A & B)

Essayer avec d'autres séquents plus difficiles.

8. Écrire prouver_min : int -> sequent -> arbre_preuve option qui, étant donné une profondeur maximale max_depth et un séquent, tente de trouver une preuve de ce séquent avec la plus petite profondeur possible (inférieure ou égale à max_depth).

prouver_min 8 (parse "|- (A & (B | C)) -> ((A & B) | (A & C))") |> Option.iter (afficher_arbre_preuve 1)

9. Quand vous avez fini, entraînez-vous sur https://fortierq.github.io/deduction-naturelle.