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 :
- Méthode des tableaux matriciels (algorithme de Quine)
- Méthode de tableaux sémantiques (Beth, Hinkita, Smullyan)
- Méthode des connexions (Bibel, Wallen)
- Méthode des ``if-expressions'' (Boyer, Moore)
- Méthode de réduction àla forme normale (Hilbert, Ackermann)
- 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 :
- (i) Les variables propositionnelles et les constantes sont en
forme canonique.
- (ii) Si p est une variable propositionnelle et c est une
constantes, si A et B sont en forme canonique alors If(p,A,B)
et If(c,A,B) sont en 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.