Programmation
et application àla démonstration automatique

DEA de logique et fondements de l'informatique
Notes de cours






I - Le calcul des propositions



On utilisera les connecteurs ¬, Ù, Ú, Þ et Û, les deux constantes propositionnelles T et F ainsi qu'un ensemble (infini dénombrable) de variables propositionnelles P. Une assignation, ou une distribution est une fonction s de P dans {T,F}. L'assignation s est étendue de façon standard aux formules. La sémantique des connecteurs est donnée par :
s(¬ A)=T, si s(A)=F s(¬ A)=F, si s(A)=T
s(AÙ B)=T, si s(A)=T et s(B)=T s(AÙ B)=F, si s(A)=F ou s(B)=F
s(AÚ B)=T, si s(A)=T ou s(B)=T s(AÚ B)=F, si s(A)=F et s(B)=F
s(AÞ B)=T, si s(A)=F ou s(B)=T s(AÚ B)=F, si s(A)=F et s(B)=T
s(AÞ B)=T, si s(A)=s(B) s(AÚ B)=F, si s(A)¹s(B)
On dit qu'une formule A est réalisable, ou encore satisfaisable, s'il existe une assignation s telle que s(A)=T. On dit qu'une formule A est valide, ou encore qu'elle est une tautologie, si pour toute assignation s, s(A)=T.



Les propositions seront représentées par le type : 
type prop =
 C of bool
|P of int
|Not of prop
|And of prop*prop
|Or of prop*prop
|Imp of prop*prop
|Equ of prop*prop
;;


On examinera six méthodes de décision :
  1. Méthode des tableaux matriciels (algorithme de Quine)
  2. Méthode de tableaux sémantiques (Beth, Hinkita, Smullyan)
  3. Méthode des connexions (Bibel, Wallen)
  4. Méthode des ``if-expressions'' (Boyer, Moore)
  5. Méthode de réduction àla forme normale (Hilbert, Ackermann)
  6. Méthode de résolution (Robinson)





§ 1. Tableaux matriciels

C'est la méthode bien connue des tables de véritéqui consiste àassigner successivement les valeurs T et F àchacunes des variables propositionnelles. Quine a améliorécette coûteuse méthode en proposant l'application de règles de simplification lors de la substitution des constantes aux variables propositionnelles. Une meilleure performance (en moyenne) est obtenue en susbtituant d'abord àla variable ayant le plus d'occurence dans la formule.



(1.a) Règles de simplifications
On écrit les régles sous la forme A¾® A', oùA et A' sont deux formules. On choisit A et A' de telle sorte que AÛ A' soit valide. Ce qui fonde la validitédes règles (théorème de remplacement). De plus, A' est une formule de taille strictement inférieure àA, ce qui assure la terminaison du processus de simplification. Les règles proposées par Quine sont :
¬F ¾® T ¬T ¾® F ¬¬ A ¾® A   -  
TÙ A ¾® A AÙT ¾® A FÙ A ¾® F AÙF ¾® F
TÚ A ¾® T AÚT ¾® T FÚ A ¾® A AÚF ¾® A
TÞ A ¾® A FÞ A ¾® T AÞT ¾® T AÞF ¾® ¬ A
TÛ A ¾® A AÛT ¾® A FÛ A ¾® ¬ A AÛF ¾® ¬ A
On dit qu'une règle est applicable àune formule si celle-ci a l'une des formes de l'un des membres gauches des régles.




(1.b) Une implémentation
On appelle S la fonction de simplification vérifiant, pour toute formule A :
  S(A) = A, si aucune r`egle n'est applicable `a A
  A¾® S(A), sinon
Etant donnée une formule A on veut itérer l'application des règles de simplification jusqu'àsaturation. On définit pour cela la fonction suivante S* telle que
  Si A=¬ A1 et si A'1= S*(A1) alors
    S*(A)=S(A'1)
  Sinon, si A=A1* A2 avec *Î{Ù,Ú,Þ,Û}, si A'1=S*(A1) et si A'2=S*(A2) alors
    S*(A)=S(A'1* A'2)
Soit alors la fonction T définie sur une formule A et un ensemble de variables propositionnelles X.
  Si A=T ou A=F ou X=Ø alors
    T(A,X)=A
  Sinon, si X={x}È X' et si A'=S(S*(A[T/x])Ù S*(A[F/x])) alors
    T(A,X)=T(A',X')
Si X est l'ensemble des varaibles propositionnelles de la formule A et si T(A,X)=T alors A est une tautologie.



(1.d) Du code


Fonction de fusion de deux listes. Si la première liste est sans duplication alors le résultat l'est aussi. 
(* merge_vars : 'a list -> 'a list -> 'a list *)
let rec merge_vars xs = function
 [] -> xs
|y::ys 
 -> if mem y xs then merge_vars xs ys else merge_vars (y::xs) ys
;;
Fonction de calcul de la liste des variables propositionnelles d'une formule. 
(* vars_of : prop -> int list *)
let rec vars_of = function
 P n -> [n]
|Not(p) -> vars_of p
|And(p1,p2) -> merge_vars (vars_of p1) (vars_of p2)
|Or(p1,p2) -> merge_vars (vars_of p1) (vars_of p2)
|Imp(p1,p2) -> merge_vars (vars_of p1) (vars_of p2)
|_ -> []
;;
Fonction S d'application d'une règle de simplification. 
(* simpl : prop -> prop *)
let simpl = function
 Not(C(false)) -> C(true)
|Imp(C(true),p) -> p
|Imp(C(false),_) -> C(true)
|Or(C(true),_) -> C(true)
|Or(_,C(true)) -> C(true)
|And(C(true),p) -> p
|And(p,C(true)) -> p
|Equ(C(true),p) -> p
|Equ(p,C(true)) -> p
|Not(C(true)) -> C(false)
|Imp(_,C(true)) -> C(true)
|Imp(p,C(false)) -> Not(p)
|Or(C(false),p) -> p
|Or(p,C(false)) -> p
|And(C(false),_) -> C(false)
|And(_,C(false)) -> C(false)
|Equ(C(false),p) -> Not(p)
|Equ(p,C(false)) -> Not(p)
|p -> p
;;
On définit la fonction S* d'itération de S en calculant àla fois un substituéet sa simplification. 
(* simpl_subst : int * bool -> prop -> prop *)
let rec simpl_subst (n,vv) = function
 P(m) -> if m=n then C(vv) else P(m)
|Not(p) -> simpl (Not(simpl_subst (n,vv) p))
|And(p1,p2)
 -> simpl (And(simpl_subst (n,vv) p1, simpl_subst (n,vv) p2))
|Or(p1,p2)
 -> simpl (Or(simpl_subst (n,vv) p1, simpl_subst (n,vv) p2))
|Imp(p1,p2)
 -> simpl (Imp(simpl_subst (n,vv) p1, simpl_subst (n,vv) p2))
|p -> p
;;
Enfin, la fonction T s'écrit 
(* it_simpl_subst : prop -> int list -> bool *)
let rec it_simpl_subst p xs =
 match p,xs with
  (C(vv),_) -> vv
 |(p,[]) -> true
 |(p,(x::xs))
  -> (it_simpl_subst (simpl_subst (x,true) p) xs)
     & (it_simpl_subst (simpl_subst (x,false) p) xs)
;;





§ 2. Les if-expressions
La méthode décrite dans ce paragraphe met en oeuvre une idée analogue àcelle du paragraphe précédent : l'assignation de valeurs de vérités aux variables propositionnelles jointe àl'utilisation de règles de simplifications.
Elle s'en distingue de deux façons :

- elle est définie sur un langage ne comportant qu'un seul connecteur ternaire (le if-then-else des langages de programmation)

- elle est définie sur une sous classe des propositions de ce langage : des expressions en forme canonique



Nous appellerons if-expressions les propositions formées sur le connecteur ternaire if-then-else, les constantes T et F et les variables propositionnelles. Pour traiter des propositions usuelles avec cette méthode, il faut donc les traduire en if-expressions puis leur appliquer un processus de normalisation avant d'en examiner la validité.



(2.a) Codage des connecteurs
On peut coder les connecteurs binaires du calcul des propositions en utilisant un seul connecteur ternaire : le if-then-else des langages de programmation. Nous noterons If  ce connecteur et If(A,B,C) son application. Sa sémantique est celle attendue :
If(T,A,B) = A
If(F,A,B) = B
Elle nous donne deux règles de simplification. La traduction des connecteurs usuels est donnée par le tableau suivant
¬ A If(A,F,T)
AÙ B If(A,B,F)
AÚ B If(A,T,B)
AÞ B If(A,B,T)
AÛ B If(A,B,If(B,F,T))



(2.b) Forme canonique
On définit par induction sur les if-expressionsune forme canonique : En utilisant les équivalences définissant la sémantique des if-expressions, ont peut définir une forme canonique réduite.


A toute if-expressions  correspond une (unique) forme canonique réduite donnée par la fonction CR définie par :
CR(p) = p
CR(c) = c
CR(If(T,A,B)) = CR(A)
CR(If(F,A,B)) = CR(B)
CR(If(p,A,B)) = If(p,CR(A),CR(B))
CR(If(If(A,B,C),D,E)) = CR(If(A,If(B,D,E),If(C,D,E)))
Rem : c'est un exercice intéressant que de prouver formellement la terminaison de la fonction CR.



(2.c) La méthode
La méthode de décision basée sur le codage des propositions par des if-expressions  est analogue àcelle que nous avons utilisée pour les tableaux matriciels : on substitue aux variables successivement les constantes T  et F  et on simplifie. La fonction S définie ci-dessous réalise cette méthode. On définit S sur les formes canoniques (non réduites àune variable propositionnelle).

  Si AÎ{T,F} alors S(A)=A;
  Si A = If(p,A1,A2) :
    si S(A1[T/p])=T alors S(A)=S(A2[F/p])
    sinon, S(A)=F



(2.d) Du code
Le type des if-expressions: 
type ifexp =
 IfC of bool
|IfP of int
|If of ifexp*ifexp*ifexp
;;
La fonction de traduction : 
(* if_of_prop : prop -> ifexp *)
let rec if_of_prop = function
 C b -> IfC b
|P n -> IfP n
|Not(p1) -> If(if_of_prop p1, IfC false, IfC true)
|And(p1,p2) 
 -> If(if_of_prop p1, if_of_prop p2, IfC false)
|Or(p1,p2) -> If(if_of_prop p1, IfC true, if_of_prop p2)
|Imp(p1,p2) -> If(if_of_prop p1, if_of_prop p2, IfC true)
|Equ(p1,p2) 
 -> let p2' = if_of_prop p2 in 
     If(if_of_prop p1, p2', If(p2', IfC false, IfC true))
;;
La fonction CR de mise en forme canonique réduite : 
(* if_norm : ifexp -> ifexp *)
let rec if_norm = function
 If(If(p1,p2,p3),p4,p5)
 -> if_norm (If(p1,If(p2,p4,p5),If(p3,p4,p5)))
|If(IfC b,p1,p2) 
 -> if b then  if_norm p1 else if_norm p2
|If(p,p1,p2) 
 -> If(p, if_norm p1, if_norm p2)
|x -> x
;;
Pour implémenter la fonction de simplification S on utilisera une substitution retardée : àchaque occurence d'une variable propositionnelle non encore rencontrée lors de la descente récursive dans l'expression, on enrichit une liste d'association liant la variable àune valeur booléenne (le paramètre nbs de notre fonction). 
(* simpl_subst : (int * bool) list -> ifexp -> bool *)
let rec simpl_subst nbs = function
 (IfP n) 
 -> (try assoc n nbs 
     with Not_found -> false)
|(IfC b) -> b
|If(IfP n,p2,p3) 
 -> (try
      if assoc n nbs then simpl_subst nbs p2
      else simpl_subst nbs p3
     with
      Not_found
      -> (simpl_subst ((n,true)::nbs) p2) 
         & (simpl_subst ((n,false)::nbs) p3))
|_ -> failwith "unexpected pattern in 'simpl_subst'"
;;
This document was translated from LATEX by HEVEA.