Algorithmes pour la logique

Christophe Raffalli

Février 1995

Table des matières

1 Introduction. 2

2 Algorithmes de Décision en Calcul Propositionnel. 2 2.1 Les formules. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Première version. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

2.2.1 Construction de l’ensemble des variables V (F). . . . . . . . . . . . . . . . . 2 2.2.2 Test de validité. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2.3 Test des tautologies. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2.4 Le source. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2.3 Les if-expressions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3.1 Définitions et principes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3.2 Davis & Putnam. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.3.3 Le source. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

2.4 Le calcul des séquents. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.4.1 Définition. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.4.2 Implémentation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.4.3 Le source. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

3 L’unification. 16 3.1 Définition. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.2 L’algorithme élémentaire. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3.2.1 Présentation de l’algorithme. . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.2.2 Implémentation de l’algorithme. . . . . . . . . . . . . . . . . . . . . . . . . 17

3.3 Unification pseudo-linéaire. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3.1 Représentation des termes par des équations. . . . . . . . . . . . . . . . . . 19 3.3.2 Présentation de l’algorithme. . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3.3 Implémentation de l’algorithme. . . . . . . . . . . . . . . . . . . . . . . . . 21

4 La résolution en calcul des prédicats. 28 4.1 La résolution binaire. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 4.2 La subsumption. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.3 “Set of support” et Hyper-résolution. . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.4 Mise sous forme clausale. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.5 Implémentation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30

A Générateur aléatoire de formules. 42

B Un chronomètre 42

C Utilisation du démonstrateur de théorèmes. 43

1 Introduction.

Le but de ce cours est de présenter quelques algorithmes simples utilisés en logique et plus précisément des méthodes utilisées en calcul propositionnel et en calcul des prédicats. Tous les algorithmes sont accompagnés d’un source en Caml-Light qu’il est aussi possible de télécharger par ftp :

     site = www.lama.univ-savoie.fr
     dir = pub/users/RAFFALLI
     file = logalgo.tar.gz

Dans une première section, on s’intéressera en détail au calcul propositionnel. Par la suite on présentera le problème de l’unification et un algorithme d’unification linéaire. Enfin, on proposera une implémentation de la résolution pour le calcul des prédicats. Les algorithmes sont présentés sans preuves de corrections ou de complétudes.

2 Algorithmes de Décision en Calcul Propositionnel.

2.1 Les formules.

Les formules sont définies inductivement à partir d’un ensemble infini de variables et des constantes 0 et 1, comme le plus petit “ensemble” clos pour les constructeurs suivants : Négation ¬F Conjonction F ∧ G Disjonction F ∨ G Implication F → G Équivalence F ↔ G

On peut les définir en Caml-Light par le type suivant :

type var == int;;
type form =
  Var of var
| Vrai | Faux
| Non of form
| Bin of conn * form * form
and conn = Et | Ou | Im | Eq
;;

On va décrire trois types d’algorithmes permettant de tester si une formule est une tautologie (une formule est une tautologie si et seulement si sa négation n’est pas satisfaisable).

2.2 Première version.

La première version consiste à utiliser directement la définition sémantique de la validité d’une formule. Il suffit de tester la valeur de cette formule pour toutes les valuations possibles de ses variables. Ceci peut être décomposé en trois étapes : Construction de l’ensemble des variables, calcul de la valeur de vérité d’une formule dans une valuation donnée et test de toutes les valuations.

2.2.1 Construction de l’ensemble des variables V (F).

Par induction sur la structure de la formule :

V (X)  = {X} si X est une variable
V (¬F)  = V (F)
V (F ⋆ G) = V (F) ∪ V (G) si ⋆ est un connecteur binaire

En Caml-Light, l’ensemble des variables peut être représenté de différentes manières :

1. En utilisant une liste de variables (la fonction union étant prédéfinie). La taille d’un ensemble et le test d’appartenance sont alors linéaires par rapport aux nombres de variables apparaissant dans F.

2. En utilisant le type set de la librairie standard. La taille étant toujours linéaire par rapport aux nombres de variables apparaissant dans F, mais le test d’appartenance devient logarithmique.

3. Par un vecteur de booléens dont le n-ème champ indique si la variable représentée par l’indice n apparaît dans F. Le test d’appartenance s’effectue alors en temps constant. En contrepartie, la taille d’un ensemble est linéaire par rapport au nombre de variables susceptibles d’apparaître dans F, et non par rapport aux nombres de variables apparaissant vraiment.

4. Par un simple entier majorant toutes les variables dans la formule. Cette représentation suppose que si la variable d’indice n apparaît dans F alors toutes les variables d’indice inférieur à n y apparaissent aussi.

En pratique, dans ce qui suit, on utilisera la liste des variables uniquement pour la parcourir, et ceci une ou deux fois. On n’a donc pas besoin d’un test d’appartenance. La première solution est donc bien suffisante.

2.2.2 Test de validité.

Pour tester si une formule est vraie dans une valuation donnée, il suffit d’utiliser la définition par induction de la vérité en calcul propositionnel. La valeur de vérité des variables étant donnée, la valeur de vérité d’une formule s’obtient pour chaque connecteur en appliquant la table de vérité de ce connecteur aux valeurs des sous-formules. On notera 𝔽^{v} la valeur d’une formule dans une valuation v.

La représentation des valuations peut se faire de différentes façons :

1. Par un liste de paires (variable × valeur) (type (var * bool) list). La fonction prédéfinie assoc permettant de tester la valeur d’une variable (Taille de la valuation et temps d’accès à la valeur sont linéaires par rapport au nombre de variables).

2. En utilisant l’une des librairies hashtbl ou map. Elles permettent un temps d’accès plus rapide en conservant une taille linéaire (attention la librairie hashtbl modifie physiquement la table des valeurs et doit donc être utilisée avec précaution).

3. Avec un tableau de booléens dont le n-ème champ indique la valeur de la variable d’indice n. Le temps d’accès étant alors constant, mais en contrepartie le tableau doit contenir toutes les variables susceptibles d’apparaître dans la formule. Cela reste linéaire si le plus grand indice d’une variable apparaissant dans la formule est linéaire par rapport au nombre de variables. En effet si les variables d’indice 1 et 3 apparaissent dans F, il est nécessaire de prévoir une place pour la variable d’indice 2 dans le tableau, même si elle n’apparaît pas dans la formule.

2.2.3 Test des tautologies.

Le problème est maintenant d’engendrer toutes les valuations. La méthode la plus simple consiste à faire une induction sur la liste des variables. On a alors besoin d’une fonction intermédiaire testant si une formule est vraie pour toutes les valuations d’un ensemble de variables, en supposant donnée une valuation pour les autres variables n’apparaissant pas dans cet ensemble. On définit par induction cette fonction T′ :

T′(F, v, {}) = 𝔽^{v}
T′(F, v, e) = T′(F, {(X, 1)} ∪ v, e − {X}) ET
T′(F, {(X, 0)} ∪ v, e − {X}) si X ∈ e

T′(F, v, e) est alors définie si et seulement si l’ensemble des variables apparaissant dans F est égal à l’union de l’ensemble e et des variables déclarées dans v. La fonction T testant si une formule est une tautologie est alors définie par

T (F) = T′(F, {}, V (F))

2.2.4 Le source.

On implémente ici les trois étapes décrites ci-avant. L’ensemble des variables étant représenté par une liste d’entiers. Les fonctions eval et taut sont paramétrées par les fonctions permettant de manipuler les valuations. On testera ainsi trois représentations pour les valuations.

(* "vars" f fabrique la liste des variables de la formule f *)
let vars f = fn f
  where rec fn = function
    Var n -> [n]
  | Vrai | Faux -> []
  | Non f -> fn f
  | Bin(_,f,g) -> union (fn f) (fn g)
;;
(* "eval getv val f" teste si f est vraie dans la valuation val de type 'a en
   utilisant la fonction getv de type var -> 'a -> bool pour aller chercher
   la valeur d'une variable *)
let eval getv val f = fn f
  where rec fn = function
    Var n -> getv n val
  | Vrai -> true
  | Faux -> false
  | Non f -> not (fn f)
  | Bin (c,f,g) -> match c with
      Et -> (fn f) & (fn g)
    | Ou -> (fn f) or (fn g)
    | Im -> not (fn f) or (fn g)
    | Eq -> (fn f) = (fn g)
;;
(* "taut init getv addone f" teste si la formule f est une tautologie en
   utilisant la fonction "getv : var -> 'a -> bool" pour aller chercher la
   valeur d'une variable, la fonction "addone : var -> bool -> 'a -> 'a"
   pour ajouter un élément à une valuation et la
   fonction "init : var list -> 'a" pour fabriquer la valuation initiale vide
*)
let taut init getv addone f =
  let lv = vars f in
  fn (init lv) lv
  where rec fn val = function
    [] -> eval getv val f
  | n::l -> (fn (addone n true val) l) & (fn (addone n false val) l)
;;
(* test des tautologies avec des listes *)
let taut_list = taut (fun _-> []) assoc (fun x b l -> (x,b)::l)
;;
(* test des tautologies avec des maps *)
let compare_int n p = if n < p then -1 else if n = p then 0 else 1;;
let taut_map = taut

  (fun _-> map__empty compare_int)
  map__find
  map__add
;;
(* test des tautologies avec des vecteurs *)
let taut_vect = taut
  (fun lv -> make_vect ((it_list max 0 lv) + 1) false)
  (fun n v -> v.(n))
  (fun n b v -> v.(n) <- b; v)
;;
(* Attention : cette dernière version n'est pas purement fonctionnelle, et
   sa correction dépend de l'ordre d'évaluation *)

(* test sur une SPARC 10, F étant une formule de longueur 1000 utilisant 12
   variables et fabriquée avec random_form (cf appendices) *)
chrono taut_list F;;
Time = 2.433333s of S+U time
- : bool = true
chrono taut_map F;;
Time = 4.600000s of S+U time
- : bool = true
chrono taut_vect F;;
Time = 1.416667s of S+U time
- : bool = true

Remarque : la version utilisant des vecteurs est bien la plus rapide. Toutefois la version utilisant des “maps” est la plus lente. Ceci s’explique car on n’utilise que des “maps” comprenant une dizaine d’entiers, et dans ce cas, utiliser des listes est aussi rapide. Pour constater un gain, il faudrait utiliser une centaine de variables, mais l’algorithme ne terminerait alors jamais son calcul !

2.3 Les if-expressions.

2.3.1 Définitions et principes

Les if-expressions sont des formules construites à partir des variables propositionnelles et des constantes vrai (⊤) et fausse (⊥) et utilisant un seul connecteur ternaire “ if P then Q else R” dont la valeur de vérité est celle de Q si P est vraie et celle de R si P est fausse.

Toute formule du calcul propositionnelle est équivalente à une if-expression. Pour prouver cela, if suffit de constater les équivalences suivantes (sachant que les connecteurs ¬,∧ et ∨ forme un ensemble complet de connecteur) :

¬P <→ if P then ⊥ else ⊤
P ∧ Q <→ if P then Q else ⊥
P ∨ Q <→ if P then ⊤ else Q

On peut alors définir les deux notions suivantes :

Une if-expression F est normale si elle vérifie les deux conditions suivantes (ou pseudo-normale si elle ne vérifie que la première) :

1. Pour toute sous-formule de F de la forme if P then Q else R, P est une variable propositionnelle.

2. Pour toute sous-formule de F de la forme if X then Q else R, la variable X n’apparaît ni dans Q ni dans R.

Il est alors facile de démontrer qu’une if-expression normale est une tautologie si et seulement si toutes ses feuilles sont égales à la constante ⊤.

Pour transformer une if-expression en une if-expression normale, il suffit d’utiliser les identités suivantes :

– if ( if P then Q else R) then Q′ else R′ <→ if P then ( if Q then Q′ else R′) else ( if R then Q′ else R′)

– if X then Q else R <→ if X then Q[X/⊤] else R[X/⊥]

Il est alors facile d’écrire un programme testant si une formule est une tautologie utilisant des if-expressions et utilisant les étapes suivantes :

1. Transformation de la formule en une if-expression.

2. Utilisation de la première identité pour obtenir une forme pseudo-normale.

3. Utilisation de la seconde identité pour obtenir une forme normale.

4. Tester si l’expression est une tautologie.

Le problème de cette approche, est que la seconde étape peut fabriquer une if-expression très grosse (taille exponentielle par rapport à la formule originale), qui se simplifie parfois énormément à la troisième étape. Il est donc nécessaire de regrouper les deuxième et troisième étapes. Pour cela, on peut remarquer que la seconde étape fabrique des if-expressions d’une forme particulière : if p[(p_{1}, q_{1}); …; (p_{n}, q_{n})], ceci étant une abréviation définie de la manière suivante :

if P [] = P
if P [(P_{1}, Q_{1}); l] = if P then ( if P_{1}[l]) else ( if Q_{1}[l])

La première identité peut alors s’écrire if ( if P then Q else R)[l] <→ if P [(Q, R); l]. On peut utiliser un “accumulateur” (paramètre auxiliaire d’un fonction) contenant une liste de couple de if-expressions, pour réaliser simultanément les seconde et troisième étapes (cf source ci-dessous). On peut tout aussi bien grouper les quatres étapes, bien que cela soit moins crucial.

2.3.2 Davis & Putnam.

Un examen attentif de l’algorithme montre qu’il n’est pas très différent du premier (testant toutes les valeurs de vérité). En effet, cette méthode choisie une variable X afin de réécrire une formule P sous la forme if X then P [X/⊤] else P [X/⊥]. Si l’on fait cela récursivement pour toutes les variables présentes dans P, on examine bien toutes les valuations. L’avantage de la méthode réside dans les implications intervenant dans P [X/⊤] et P [X/⊥], qui peuvent faire disparaître certaines variables ce qui permet de traiter simultanément certaines valuations. La méthode des if-expressions sans le calcul des if-expressions, s’appelle la méthode de Davis & Putnam et est réputé pour être l’une des plus efficace.

L’important dans cette méthode, est le choix de la variable de tête à chaque étape. La méthode exposée ci-dessus réalise un choix aveugle (mais ne coûtant rien). Il peut aussi être payant de passer du temps à calculer une bonne variable de tête, par exemple en choisissant la variable X minimisant le nombre de variables apparaissant dans les deux formules P [X/⊤] et P [X/⊥] après simplification (cf source ci-dessous).

2.3.3 Le source.

(* type décrivant les if-expressions *)
type if_expr =
  iVrai | iFaux | iVar of int
| If of if_expr * if_expr * if_expr
;;

(* form_to_normal_if p fabrique une if-expression normale équivalente
 à la formule p *)
let form_to_normal_if p =
(* sachant que
     - tbl est une valuation partielle associant un booléen à
       certaines variables propositionnelles
     - l est une liste de paires de formules
   fn tbl l p, fabrique une if-expression équivalente à la formule
   IF(p,l) où les variables déclarées dans tbl substituées par leur valeur.
   IF(p,l) étant définit par
     - IF(p,[]) = p
     - IF[p,(p1,q1)::l] = if p then IF[p1,l] else IF[q1,l]
*)
let rec fn tbl l = function
  Vrai -> gn tbl true l
| Faux -> gn tbl false l
| Var n -> (
   try gn tbl (assoc n tbl) l
   with Not_found -> If (iVar n, gn ((n,true)::tbl) true l,
                                gn ((n,false)::tbl) false l))
| Bin (Et,p1,p2) -> fn tbl ((p2,Faux)::l) p1
| Bin (Ou,p1,p2) -> fn tbl ((Vrai,p2)::l) p1
| Bin (Im,p1,p2) -> fn tbl ((p2,Vrai)::l) p1
| Bin (Eq,p1,p2) -> fn tbl ((p2,Non p2)::l) p1
| Non (Non p1) -> fn tbl l p1
| Non p1 -> fn tbl ((Faux,Vrai)::l) p1
and gn tbl b = function
  [] -> if b then iVrai else iFaux
| (p1,p2)::l' -> if b then fn tbl l' p1
                      else fn tbl l' p2
in fn [] [] p
;;
(* taut_if p vérifie que p est une tautologie, en utilisant le même
algorithme que la fonction précédente, mais sans calculer la
if-expression. La fonction vérifie simplement que si la if-expression
avait été construite, toutes ses feuilles seraient égales à Vrai (ce
qui pour une if-expression normale est équivalent à dire qu'il s'agit
d'une tautologie *)
let taut_if p =
let rec fn tbl l = function
  Vrai -> gn tbl true l
| Faux -> gn tbl false l
| Var n -> (
   try gn tbl (assoc n tbl) l
   with Not_found -> gn ((n,true)::tbl) true l & gn ((n,false)::tbl) false l)
| Bin (Et,p1,p2) -> fn tbl ((p2,Faux)::l) p1
| Bin (Ou,p1,p2) -> fn tbl ((Vrai,p2)::l) p1
| Bin (Im,p1,p2) -> fn tbl ((p2,Vrai)::l) p1

| Bin (Eq,p1,p2) -> fn tbl ((p2,Non p2)::l) p1
| Non (Non p1) -> fn tbl l p1
| Non p1 -> fn tbl ((Faux,Vrai)::l) p1
and gn tbl b = function
[] -> b
| (p1,p2)::l' -> if b then fn tbl l' p1
                    else fn tbl l' p2
in fn [] [] p
;;
(* simplify tbl p simplifie une formule p sachant que certaines
variables sont égales à Vrai ou Faux, comme indiqué dans tbl.
tbl est un tableau d'objets du type val défini ci dessous. *)
type val =
ValVrai
| ValFaux
| NoVal
| NoOcc;;
let simplify tbl p =
let rec fn = function
Vrai | Faux as p -> p
| Var n as p -> (match tbl.(n) with
               ValVrai -> Vrai
             | ValFaux -> Faux
             | _-> p)
| Non p as pt -> (match fn p with Vrai -> Faux | Faux -> Vrai | _-> pt)
| Bin(c,p1,p2) as p -> match (c,fn p1,fn p2) with
  (Et,Vrai,p2) -> p2
| (Et,p1,Vrai) -> p1
| (Et,Faux,_)  -> Faux
| (Et,_,Faux)  -> Faux
| (Ou,Faux,p2) -> p2
| (Ou,p1,Faux) -> p1
| (Ou,Vrai,_)  -> Vrai
| (Ou,_,Vrai)  -> Vrai
| (Im,Faux,p2) -> Vrai
| (Im,Vrai,Faux) -> Faux
| (Im,p1,Faux) -> Non p1
| (Im,Vrai,p2)  -> p2
| (Im,p1,Vrai)  -> Vrai
| (Eq,Vrai,p2) -> p2
| (Eq,p1,Vrai) -> p1
| (Eq,Faux,Faux) -> Vrai
| (Eq,p1,Faux) -> Non p1
| (Eq,Faux,p2) -> Non p2
| (_,p1',p2') as p' -> if p1 == p1' & p2 == p2' then p else Bin p'

  in fn p
;;
(* type permettant de dire si une variable occurre positivement,
   négativement ou les deux dans une formule *)
type occ_typ = Neg | Pos | Both;;
(* action de la négation sur le type d'occurrence *)
let neg_occ = function
  Neg -> Pos
| Pos -> Neg
| Both -> Both
;;
(* action de la conjonction ou de la disjonction sur le type d'occurrence *)
let merge_occ = fun
  Neg Neg -> Neg
| Pos Pos -> Pos
| __-> Both
;;
(* type décrivant des formules :
   - Bool true   décrit une formule vrai
   - Bool false  décrit une formule fausse
   - Form l décrit une formule ayant au moins une variable libre.
   l est une liste de couples (v,t) où v est une des variables
   libres de la formule et t le type d'occurrence de cette variable.
   Les variables libres de la formule sont toutes présentes exactement
   une fois dans l et ordonnées en ordre croissant *)
type mini_prop =
  Bool of bool
| Form of (var*occ_typ) list
;;
(* union_sort b l l' : calcule l'union des deux listes de variables l
et l' en supposant que l et l' sont triées en ordre croissant. le
résultat étant lui aussi trié. Les informations correspondant à la
positivité des occurrences sont regroupés en utilisant merge_occ *)
let rec union_sort = fun
  [] l -> l
| l [] -> l
| ((n,t as c)::l as l0) ((n',t' as c')::l' as l0') ->
    if n < n' then c::(union_sort l l0')
    else if n > n' then c'::(union_sort l0 l')
    else (n, merge_occ t t')::(union_sort l l')
;;
(* similaire à union_sort, mais les informations de type sont fixées a
Both (utilisé pour l'équivalence) *)

let rec eq_union_sort = fun
  [] l -> l
| l [] -> l
| ((n,t as c)::l as l0) ((n',t' as c')::l' as l0') ->
    if n < n' then c::(union_sort l l0')
    else if n > n' then c'::(union_sort l0 l')
    else (n, Both)::(union_sort l l')
;;
(* action de la conjonction sur deux mini-formules *)
let mand = fun
  (Bool false as p) _-> p
| _(Bool false as p) -> p
| (Bool true as p) (Bool true) -> p
| (Bool _) (Form l as p) -> p
| (Form l as p) (Bool _) -> p
| (Form l) (Form l') -> Form (union_sort l l')
;;
(* action de la disjonction sur deux mini-formules *)
let mor = fun
  (Bool true as p) _-> p
| _(Bool true as p) -> p
| (Bool false as p) (Bool false) -> p
| (Bool _) (Form l as p) -> p
| (Form l as p) (Bool _) -> p
| (Form l) (Form l') -> Form (union_sort l l')
;;
(* action de la négation sur une mini-formule *)
let mnot = function
  Bool b -> Bool (not b)
| Form l -> Form (map (function n,t -> n, neg_occ t) l)
;;
(* action de l'implication sur deux mini-formules *)
let mim p q = mor (mnot p) q
;;
(* action de l'équivalence sur deux mini-formules *)
let meq = fun
| (Bool b) (Bool b') -> Bool (b = b')
| (Bool b) (Form l as p) -> if b then p else mnot p
| (Form l as p) (Bool b) -> if b then p else mnot p
| (Form l) (Form l') -> Form (eq_union_sort l l')
;;
(* calcule la mini_prop décrivant une formule *)

let rec prop_to_miniprop = function
  Var n -> Form [n,Pos]
| Vrai -> Bool true
| Faux -> Bool false
| Non f -> mnot (prop_to_miniprop f)
| Bin (c,f,f') ->
      (match c with Et -> mand | Ou -> mor | Im -> mim | Eq -> meq)
      (prop_to_miniprop f) (prop_to_miniprop f')
;;
(* renvoie la variable d'indice maximum apparaissant dans f *)
let max_var f =
  let rec max cur = function
     Var n -> if n < cur then cur else n
   | Vrai | Faux -> cur
   | Non f -> max cur f
   | Bin(_,p1,p2) -> max (max cur p1) p2
  in max (-1) f
;;
(* construit une valuation : si une variable X occurre
   positivement (resp. négativement) dans F, F est une
   tautologie si et seulement si F[X/Faux] (resp. Vrai)
   en est une aussi. *)
let rec mkval max_var l =
  let tbl = make_vect (max_var+1) NoVal in
  let trv = ref false in
  let rec fn = function
  [] -> ()
| (n,Pos)::l -> tbl.(n) <- ValFaux; trv := true; fn l
| (n,Neg)::l -> tbl.(n) <- ValVrai; trv := true; fn l
| (n,Both)::l -> fn l
  in fn l; tbl, !trv
;;
(* simplifie une formule en utilisant le principe ci-dessus jusqu'à ce
   que toutes les variables libres occurrent à la fois positivement et
   négativement. Attention, la formule résultante n'est PAS
   équivalente à la formule de départ. On ne peut donc pas utiliser
   cette simplification pour calculer une if-expression équivalente à
   une formule donnée. La formule simplifiée ainsi que le nombre de
   variables distinctes y apparaissant sont retournés *)
let rec rec_simplify max_var f =
  let mp = prop_to_miniprop f in
  match mp with
    Bool true -> Vrai, 0
  | Bool false -> Faux, 0
  | Form l ->
      let val, b = mkval max_var l in
      if b then rec_simplify max_var (simplify val f) else f, list_length l

;;
(* calcule quelles variables occurrent dans f. Le résultat est placé
dans un tableau en utilisant le constructeur NoOcc pour les variables
sans occurrence et le constructeur NoVal pour les autres *)
let vars max_var f =
  let vars = make_vect (max_var + 1) NoOcc in
  let rec set_vars = function
     Var n -> vars.(n) <- NoVal
   | Vrai | Faux -> ()
   | Non f -> set_vars f
   | Bin(_,p1,p2) -> set_vars p1; set_vars p2
  in set_vars f; vars
;;
(* choisit la "meilleur variable". C'est à dire la variable X pour la
   quelle si l'on considere nn = nbr de vars dans F[X<-Vrai] après
   simplification et np = nbr de vars dans F[X<-Vrai] après
   simplification, alors 2^nn + 2^np est minimum. On utilise le fait
   que log_2 (2^nn + 2^np) = max nn np + log_2 (1 + 4^-|nn-np|) afin
   d'éviter les overflows si l'on a plus de mille variables
*)
let best_choice max_var f =
  let tbl = vars max_var f in
  let best = ref (Faux,Faux) in
  let bval = ref (float_of_int (2 + max_var)) in
  for i = 0 to max_var do
    if tbl.(i) <> NoOcc then begin
      tbl.(i) <- ValVrai;
      let fp,np = rec_simplify max_var (simplify tbl f) in
      tbl.(i) <- ValFaux;
      let fn,nn = rec_simplify max_var (simplify tbl f) in
      tbl.(i) <- NoVal;
      let n' = (float_of_int (max nn np))
               +. log (1. +. power 4. (-. (float_of_int (abs(nn-np)))))
                  /. log 2. in
      if n' <. !bval then (best := fp,fn; bval := n')
    end
  done;
  !best
;;
(* La fonction vérifiant si f est une tautologie ... *)
let rec taut_good_if f =
  let max_var = max_var f in
  let rec fn = function
      Vrai -> true
    | Faux -> false
    | f ->
        let f,f' = best_choice max_var f in
        fn f & fn f'

  in fn f
;;
(* cet algorithme peut être optimiser car l'on parcours trop souvent
la formule. On peut grouper certains calculs et conserver des
informations à chaque noeud de la formule (tel que la mini_prop
associée au noeud, car l'on fait de nombreuse fois le même calcul
lorsqu'une sous-formule reste inchangée pendant quelques temps). Cela
devrait faire gagner un facteur constant assez important. *)
(* test sur une Sparc 10 avec des ensembles de clauses de taille 3
générées aléatoirement (cf appendix).
20 variables 150 clauses de taille 3
#let f = random_form 20 150 3;;
#chrono taut_good_if f;;
Time = 78.216667s of S+U time
- : bool = true
#chrono taut_if f;;
Time = 59.083333s of S+U time
- : bool = true
pas encore assez de variables ...
30 variables 150 clauses de taille 3
#let f = random_form 30 150 3;;
#chrono taut_good_if f;;
Time = 386.750000s of S+U time
- : bool = true
#chrono taut_if f;;
Time > 1200s of real time
40 variables 150 clauses de taille 3
#let f = random_form 40 150 3;;
#chrono taut_good_if f;;
Time = 82.9666666667s of S+U time
- : bool = false
#chrono taut_if f;;
Time > 1200s of real time
*)

2.4 Le calcul des séquents.

2.4.1 Définition.

Un séquent est une “expression” de la forme

P_{1}, …, P_{n} ⊢ Q_{1}, …, Q_{m}

P_{1}, …, P_{n} et Q_{1}, …, Q_{m} étant des formules du calcul propositionnel. On considérera la partir gauche et droite d’un séquent comme des ensembles de formules (l’ordre et les duplications n’importent donc pas).

On dira qu’un séquent est prouvable, si il peut-être obtenu en utilisant les règles de dérivation suivante (on notera Γ ou Δ des ensembles de formules) :

\begin{aligned}& Ax \\ Γ, P ⊢ P, Δ \end{aligned}  \begin{aligned}& Ax \\ Γ ⊢ ⊤, Δ \end{aligned}  \begin{aligned}& Ax \\ Γ, ⊥ ⊢ Δ \end{aligned}
Γ, P ⊢ Δ ; ¬_{r} ; Γ ⊢ ¬P, Δ  Γ ⊢ P, Δ ; ¬_{l} ; Γ, ¬P ⊢ Δ

Γ ⊢ P, Δ  Γ ⊢ Q, Δ ; ∧_{r} ; Γ ⊢ P ∧ Q, Δ  Γ, P, Q ⊢ Δ ; ∧_{l} ; Γ, P ∧ Q ⊢ Δ

Γ ⊢ P, Q, Δ ; ∨_{l} ; Γ ⊢ P ∨ Q, Δ  Γ, P ⊢ Δ  Γ, Q ⊢ Δ ; ∨_{l} ; Γ, P ∨ Q ⊢ Δ

Les règles pour les autres connecteurs peuvent se déduire des précédentes en utilisant la définition de ces connecteurs à partir de la négation, conjonction et disjonction.

On peut démontrer les résultats suivants sur cette présentation du calcul des séquents : Toutes les règles sont inversibles, c’est à dire que le séquent conclusion est équivalent^{1} à la conjonction des séquents prémices de la règle (ou est vrai si la règle n’a pas de prémices). De plus chaque règle introduit un nouveau connecteur. Cela implique que l’on ne peut pas construire de branche infinie en partant de la conclusion et en appliquant des règles. On en déduit que ce système de déduction est correct et complet pour le calcul propositionnel (P est une tautologie si et seulement si ⊢ P est prouvable).

2.4.2 Implémentation.

Il est facile de produire un algorithme testant si une formule est une tautologie à partir du calcul des séquents. Il suffit de partir de la conclusion (initialement un séquent de la forme ⊢ P) et d’appliquer n’importe quelle règle. Toutefois on peut utiliser les critères suivants pour choisir la règle plus efficacement :

– Il faut retarder au maximum les applications de règles binaires.

– La présence d’un axiome peut être tester à plusieurs moment. Une méthode raisonnable est de ne faire ce test qu’avant d’appliquer une règle binaire. De plus ce test est plus efficace si l’on ne recherche que les axiomes concernant des variables (bien sur les preuves peuvent alors être beaucoup plus longues).

– On peut repousser toutes les négations au niveau atomique ce qui permet de ne considérer que les règles droites du calcul (sauf pour la négation, à moins de changer l’axiome en ⊢ Γ, P, ¬P).

On peut suggérer quelques optimisations (non implémentées dans le source ci-dessous) :

– Si une variable apparaît à droite du séquent, on peut l’éliminer en lui substituant la constant ⊥ et ainsi simplifier le séquent.

– Si une variable apparaît à gauche du séquent, on peut l’éliminer en lui substituant la constant ⊤ et ainsi simplifier le séquent.

– On peut utiliser des heuristiques pour choisir la règle binaire à appliquer. Un choix raisonnable en présence des optimisations ci-dessus est de prendre la plus petite formule.

2.4.3 Le source.

(* Type des formules avec disjonctions et conjonctions n-aires au lieu
   de binaire, toutes les négations étant ramenées au niveau atomique *)
type multi_prop =
  Dis of multi_prop list (* disjonction *)
| Con of multi_prop list (* conjonction *)
| pVar of int            (* variable *)
| nVar of int            (* négation d'une variable *)

1le séquent P_{1}, …, P_{n} ⊢ Q_{1}, …, Q_{m} est considéré équivalant à la formule (P_{1} ∧ … ∧ P_{n}) → (Q_{1} ∨ … ∨ Q_{m})

| sVrai | sFaux
;;
(* prop_to_multi_prop p transforme une formule de type prop en une
formule de type multi_prop. La traduction du connecteur Eq depend de
sa positivité dans la formule afin qu'une règle binaire soit appliquée
en premier (donnat un branchement moindre dans la preuve *)
let prop_to_multi_prop p =
let rec fn pos b p =
  let rec fd l = fun
    true (Bin (Ou,p1,p2)) -> fd (fd l true p1) true p2
  | false (Bin (Et,p1,p2)) -> fd (fd l false p1) false p2
  | true (Bin (Im,p1,p2)) -> fd (fd l false p1) true p2
  | true (Bin (Eq,p1,p2)) -> fd (fd l true (Bin (Et,p1,p2)))
                                true (Bin (Et,Non p1,Non p2))
  | false (Bin (Eq,p1,p2)) -> fd (fd l false (Bin (Im,p1,p2)))
                                false (Bin (Im,p2,p1))
  | b (Non p1) -> fd l (not b) p1
  | b p1 -> (gn (pos = b) p1)::l
  in fd [] b p
and gn pos = function
  Var n -> if pos then pVar n
                  else nVar n
| Bin ((Ou|Im),_,_) as p -> let l = fn pos true p in
                     if pos then Dis l else Con l
| Bin ((Et|Eq),_,_) as p -> let l = fn (not pos) false p in
                     if pos then Con l else Dis l
| Non p -> gn (not pos) p
| Vrai -> sVrai
| Faux -> sFaux
in gn true p
;;
(* test si une formule est une tautologie (aucune optimisation, à par
 l'application en premier des règles unaires). Les variables
 rencontrées dans le sequent sont placés dans une "map-table" tbl
 afin d'accelérer la recherche des axiomes *)
let taut_seq p =
(* règles unaires et axiomes *)
let rec fd tbl l = function
  [] -> fc tbl l
| (Dis l'')::l' -> fd tbl l (l''@l')
| (Con _as p)::l' -> fd tbl (p::l) l'
| (pVar n)::l' -> (try
                    let b = map__find n tbl in
                    if b then fd tbl l l' else true
                  with Not_found ->
                    fd (map__add n true tbl) l l')
| (nVar n)::l' -> (try
                    let b = map__find n tbl in
                    if b then true else fd tbl l l'

                    with Not_found ->
                      fd (map__add n false tbl) l l')
  | sVrai::l' -> true
  | sFaux::l' -> fd tbl l l'
  (* règles binaires *)
  and fc tbl = function
    [] -> false
  | (Con l)::l' -> it_list (fun b p ->
                     if b then fd tbl l' [p]
                     else false) true l
  | _-> raise (Failure "bug in sdecide")
  in fd (map__empty (prefix -)) [] [(prop_to_multi_prop p)]
;;

3 L’unification.

3.1 Définition.

Les termes sont définis par induction à partir d’un ensemble de variables et d’un ensemble de symboles de fonction d’arité donnée :

– x est un terme si x est une variable.

– f(t_{1}, …, t_{n}) est un terme si f est un symbole de fonction d’arité n et si t_{1}, …, t_{n} sont des termes.

On appelle substitution une application σ de l’ensemble des variables dans l’ensemble des termes. Une telle substitution σ est étendue par induction à l’ensembles des termes en posant

σf(t_{1}, …, t_{n}) = f(σt_{1}, …, σt_{n}).

On notera σ∘σ′ la composition des substitutions ((σ∘σ′)u = σ(σ′u)), et [x ← u] la substitution σ définit par σx = u et σy = y si y ≠ x.

On considère alors le problème de l’unification et celui du pattern-matching qui sont les suivants :

– Deux termes u et v sont unifiables si et seulement si il existe une substitution σ tel que σu = σv. On peut démontrer que si u et v sont unifiables, alors il existe un unificateur le plus général σ tel que pour tout unificateur σ′ de u et v, il existe une substitution σ′′ tel que σ′ = σ′′ ∘ σ.

– le terme v “matche” le terme u si et seulement si il existe une substitution σ tel que σu = v. Dans ce cas, si il existe deux substitutions différentes qui conviennent, alors elles coïncident sur l’ensemble des variables apparaissant dans u.

Il faut noter que le pattern-matching peut toujours se ramener à un problème d’unification, il suffit de considérer les variables du second terme (celui auquel on n’applique pas de substitution) comme de nouvelles constantes de fonction d’arité 0.

Dans ce qui suit, on notera E ⊎ E′ la réunion disjointe de deux ensembles. C’est à dire que E ⊎ E′ = E ∪ E′ mais que l’on ne l’écrit de la première manière que si E ∩ E′ = ∅.

3.2 L’algorithme élémentaire.

3.2.1 Présentation de l’algorithme.

Pour résoudre le problème de l’unification, on considère le problème un peu plus générale qui consiste à résoudre un système d’équations. C’est à dire, étant donnés des termes u_{1}, …, u_{n} et v_{1}, …, v_{n}, existe-t’il une substitution σ tel que σu_{1} = σv_{1}, …, σu_{n} = σv_{n}.

L’algorithme élémentaire peut alors être décomposé de la manière suivante : À chaque étape, on considère un ensemble d’équations E et une substitution σ vérifiant la propriété suivantes : Si une variable x apparaît dans E, alors σx = x.

L’algorithme s’obtient alors en appliquant tant que possible les opérations suivantes :

– Si E = E′ ⊎ {f(u_{1}, …, u_{n}) = g(v_{1}, …, v_{p})} :

– si f = g, alors n = p et on remplace E par E′ ∪ {u_{1} = v_{1}, …, u_{n} = v_{n}}.

– sinon, il y a échec de l’unification par “clash”.

– Si E = E′ ⊎ {x = x} alors E est remplacé par E′.

– Si E = E′ ⊎ {x = u} ou E = E′ ⊎ {u = x} avec u ≠ x :

– si la variable x n’apparaît pas dans u, σ est remplacé par [x ← u] ∘ σ et E est remplacé par [x ← u]E′.

– sinon il y a échec de l’unification par “occur check”. Cette procédure termine car dans le premier cas le nombre de symboles de fonction apparaissant

dans E décroit et le nombre de variables reste inchangé, dans le second cas le nombre d’équations décroit et le nombre de variables ainsi que le nombre de symboles de fonction reste constant, tandis que dans le troisième cas le nombre de variables décroit. On en déduit donc que le triplet (nb. de variables dans E, nb. de symboles dans E, nb. d’équations dans E) décroit pour l’ordre lexicographique.

La procédure se termine lorsque E est vide ou quand un échec est rencontré. De plus on peut démontrer qu’elle se termine sans échec si et seulement si le système E de départ est unifiable, la substitution σ obtenu à la fin étant alors l’unificateur le plus général de E.

Il est important de noter que sans le test de l’occur-check cet algorithme est incorrect et peut ne pas terminer !

3.2.2 Implémentation de l’algorithme.

(* type des termes utilisant le type 'a pour représenter les
   constructeurs.  Attention : On utilise l'égalité physique pour
   comparer les constructeurs ! *)
type 'a term =
  Fun of ('a * 'a term list)
| Var of int
;;
(* type des substitutions. On supposera les variables en ordre
   strictement croissant afin d'avoir une composition plus rapide. *)
type 'a subst == (int * 'a term) list;;
(* la fonction assoc tirant partie de l'ordre *)
let ord_assoc n l = fn l
  where rec fn = function
  [] -> raise Not_found
| (n',t)::l ->
    if n' = n then t
    else if n < n' then raise Not_found
    else fn l
;;
(* Une fonction merge utilisant l'ordre et ne gardant que la première
   occurence d'une variable n (important pour la composition des
   substitutions). *)

let rec ord_merge = fun
  [] l -> l
| l [] -> l
| ((n,_as c)::l as l0) ((n',_as c')::l' as l0') ->
  if n = n' then c::(ord_merge l l')
  else if n < n' then c::(ord_merge l l0')
  else c'::(ord_merge l0 l')
;;
(* Application d'une substitution à un terme *)
let subst sigma t =fn t
  where rec fn = function
    Var n as t -> (try ord_assoc n sigma with Not_found -> t)
  | Fun (i,l)  -> Fun (i, map fn l)
;;
(* Composition de deux substitutions (Attention ce n'est pas aussi simple
   qu'il y parait, cf les détails de ord_merge) *)
let compose sigma' sigma =
  ord_merge (map (function n,t -> n,subst sigma' t) sigma) sigma'
;;
(* Test d'occurrence *)
let occur n t = fn t
  where rec fn = function
    Var n' -> n = n'
  | Fun(_,l) -> exists fn l
;;
(* Unification d'une liste d'équations (paire de termes). La
   substitution partiellement construite est conservé en premier
   argument.  *)
exception Clash;;
exception Occur_check;;
let rec unifs sigma = function
  [] -> sigma
| (Fun(i,l),Fun(i',l'))::eqs ->
    if i == i' then unifs sigma ((combine (l,l'))@eqs)
    else raise Clash
| (Var x,t)::eqs ->
    if t = Var x then unifs sigma eqs else begin
      if occur x t then raise Occur_check;
      let s = [x,t] in
      unifs (compose s sigma)
            (map (function t,t' -> subst s t, subst s t') eqs)
    end
| (t, Var x)::eqs ->
    if t = Var x then unifs sigma eqs else begin

      if occur x t then raise Occur_check;
      let s = [x,t] in
      unifs (compose s sigma)
            (map (function t,t' -> subst s t, subst s t') eqs)
    end
;;
(* Unification de deux termes *)
let unif u v = unifs [] [u,v];;
(* examples *)
let f u = Fun("f", [u]);;
let g u = Fun("g", [u]);;
let h u v = Fun("h", [u;v]);;
let x = Var 0 and y = Var 1 and z = Var 2 and s = Var 3 and t = Var 4;;
unif (f x) (g x);;
unif (f (f x)) (f y);;
unif (f (f x)) (f x);;
unif (h x (h x x)) (h (h z z) y);;
unif (h x (h x x)) (h (h z z) x);;
(* Une série exponentielle *)
unif (h x (h y y)) (h (h y y) x);;
unif (h x (h y (h z z))) (h (h (h z z) y) x);;
unif (h x (h y (h z (h s s)))) (h (h (h (h s s) z) y) x);;
unif (h x (h y (h z (h s (h t t))))) (h (h (h (h s (h t t)) z) y) x);;

3.3 Unification pseudo-linéaire.

3.3.1 Représentation des termes par des équations.

Le principe de cet algorithme est d’utiliser une représentation des termes permettant de partager au maximum des sous-termes. Ceci permet d’obtenir un algorithme ne nécessitant pas “l’occurcheck” pour terminer, celui-ci pouvant alors être testé à la fin.

Afin de considérer le partage, on représente un terme par un ensemble E d’équations de la forme x = y ou x = f(x_{1}, …, x_{n}). De plus, on suppose que chaque variable apparaît une unique fois en position de membre gauche et l’on distingue une variable “racine du terme”.

Pour utiliser cette représentation, il faut donc introduire une variable pour chaque noeud du terme, les vraies variables correspondant alors aux variables qui n’apparaissent pas comme membre gauche d’une équation. Ainsi le terme h(f(x), f(x)) peut être représenté par les équations x_{0} = h(x_{1}, x_{1}), x_{1} = f(x), x_{0} étant la racine du terme.

Cette représentation est analogue à une structure de graphe orienté. Chaque variable peut être considérée comme un noeud du graphe, tandis que les équations correspondent aux arêtes.

Il faut noter que cette représentation des termes par des équations peut faire gagner un gain exponentiel en mémoire grâce au partage et que c’est pour cela que l’on peut obtenir un algorithme linéaire pour l’unification.

Dans cette représentation, les équations de la forme x = y ne sont pas nécessaires pour représenter les termes, mais elles interviennent naturellement dans l’algorithme d’unification.

Le terme T (x, E) représenté par un ensemble d’équations E et la racine x peut être définit formellement de la manière suivante :

– T (x, E) = x si x n’apparaît pas comme membre gauche d’une équation.

– T (x, E) = T (y, E) si x = y apparaît dans E.

– T (x, E) = f(T (x_{1}, E), …, T (x_{n}, E)) si x = f(x_{1}, …, x_{n}) apparaît dans E.

Cette fonction T n’est pas toujours définie. Pour qu’elle soit définie il faut et il suffit que l’ordre <_{E}^{0} définit ci-dessous, restreint à l’ensembles des variables y tel que y <_{E}^{0} x, soit cyclique (c’est à dire que sa clôture transitive est bien fondée). On définit les ordres <_{E}^{0} et <_{E}^{1} comme les plus petites relations vérifiant les propriétés suivantes :

– si x = y ∈ E alors y <_{E}^{0} x et y <_{E}^{1} x.

– si x = f(x_{1}, …, x_{n}) ∈ E alors x_{i} <_{E}^{0} x pour 1 ≤ i ≤ n.

À partir de maintenant, on ne considérera que des ensembles d’équations E tels que <_{E}^{1} soit acyclique. L’algorithme d’unification conservera cette propriété et cette condition sera vérifiée au départ (en général le système d’équations initial ne contient pas d’équations de la forme x = y et <_{E}^{1} est la relation vide).

Le fait que T (x, E) soit bien défini (c’est-à-dire le fait que l’ordre <_{E}^{0} restreint à l’ensembles des variables y tel que y <_{E}^{0} x soit acyclique) peut être tester en temps linéaire. Il suffit de parcourir le graphe représenté par les équations en partant de la racine et en se rappelant des noeuds déjà visités. Si l’on est en train d’examiner la position courante y, il faut distinguer les variables qui sont sur le chemin de la racine à y et les autres noeuds déjà visités. Si y est une variable du premier type, on a détecté un cycle (y est sur le chemin de y à la racine), tandis que si y est du second type, on peut simplement éviter de parcourir le sous-graphe ayant pour racine y.

Lorsque la condition d’acyclicité n’est pas vérifiée, l’ensemble d’équations E avec la racine x décrivent un type de termes infinis que l’on appelle “termes rationnels”.

Tester la condition d’acyclicité va remplacer “l’occur-check” dans l’algorithme d’unification. En fait l’algorithme d’unification sans le test d’acyclicité est une algorithme d’unification pour les termes rationnels.

3.3.2 Présentation de l’algorithme.

Pour décrire l’algorithme, on définit d’abord une fonction auxiliaire G qui associe à une variable et un ensemble d’équations une autre variable et un nouvel ensemble d’équations. G(x, E) est définie de la manière suivante : si il existe une variable y tel que E = {x = y} ⊎ E′ alors on calcule (z, E′′) = G(y, E) et on définit G(x, E) = (z, {x = z} ⊎ (E′′ − {x = y})) ; sinon G(x, E) = (x, E).

Cette fonction G est bien définie car l’ordre <_{E}^{1} est supposé acyclique. De plus on vérifie facilement que G préserve cette condition. Le fait que G modifie, dans certains cas, le système d’équations est essentiel pour que l’algorithme soit linéaire (voir plus loin). De plus si G(x, E) = (y, E′) alors y n’apparaît pas comme membre gauche d’une équation de la forme y = z dans E′ (on peut en déduire que G est idempotente).

L’algorithme d’unification U considère un ensemble d’équations (contenant les équations des deux termes à unifier) et deux variables (les racines de chaque terme) et renvoie un nouvel ensemble d’équations. U(x, y, E) est définie de la manière suivante : on considère (x′, F) = G(x, E) et (y′, E′) = G(y, F) et l’on utilise la première possible des règles suivantes :

– Si x′ = y′ alors U(x, y, E) = E′.

– Si E′ = {x′ = f(x_{1}, …, x_{n}), y′ = g(y_{1}, …, y_{p})} ⊎ E_{0} alors – si f ≠ g on a échec par “clash”

– sinon on a n = p et l’on définit U par

E_{1} = {x′ = y′, y′ = g(y_{1}, …, y_{n})} ⊎ E_{0} , E_{i+1} = U(x_{i}, y_{i}, E_{i}) et U(x, y, E) = E_{n+1}

– Si x′ n’apparaît pas comme membre gauche d’une équation alors

U(x, y, E) = {x′ = y′} ⊎ E′

– Si y′ n’apparaît pas comme membre gauche d’une équation alors

U(x, y, E) = {y′ = x′} ⊎ E′

– Il n’y a pas d’autres cas car x′ et y′ sont renvoyées par G et n’apparaissent donc pas comme membre gauche d’une équation de la forme x′ = z ou y′ = z.

Cette fonction U termine, car dans chaque appel récursif le nombre K de symboles de fonction additionné au nombre de variables n’apparaissant pas comme membre gauche d’une équation décroit et car elle préserve la condition d’acyclicité de <_{E}^{1} garantissant la terminaison de G. De plus ce nombre K est proportionnel à la taille des termes à unifier. Donc si l’on oublie les appels à G, l’algorithme est bien linéaire. Pour borner le nombre d’appels à G, il faut faire un travail plus fin que nous ne décrirons pas ici.

Si u = T (x, E) et v = T (y, E) sont bien définis, on peut démontrer que u et v sont unifiables si et seulement si U(x, y, E) réussit (pas de “clash”) et donne un ensemble d’équations E′ vérifiant la condition d’acyclicité de l’ordre <_{E′}^{0} pour la racine x (remplace “l’occur-check”). De plus, si σ est l’unificateur le plus général de u et v, on a T (x, E′) = σu = σv.

Cet algorithme est facilement modifié pour obtenir un algorithme de pattern-matching ou un test d’égalité restant linéaire (tester l’égalité de T (x, E) et T (y, E′) ne serait pas linéaire). Il suffit de considérer certaines variables comme des constantes.

3.3.3 Implémentation de l’algorithme.

Une manière très efficace d’implémenter cet algorithme consiste à représenter une variable x par une référence pouvant pointer sur l’un des objets suivants :

– Unknown indiquant que la variable x n’apparaît pas comme membre gauche d’une équation.

– Link y pour une équation x = y.

– Cst (f,[x_1;\dots;x_n]) pour une équation x = f(x_{1}, …, x_{n}) Cette représentation physique du graphe permet d’effectuer toutes les manipulations nécessaires en temps constant pour implémenter les fonctions U et G. Par contre, pour obtenir un test de bonne fondaison linéaire, il faut décorer chacune des références/variables par des champs booléens permettant de noter si l’on est déjà passé par ce noeud.

Un inconvénient de cette programmation impérative est qu’il est en pratique nécessaire de fabriquer des copies ou de pouvoir défaire les modifications introduite par l’unification afin de pouvoir conserver les termes originaux (on peut se contenter de copier, mais en cas d’échec rapide fréquent, la seconde méthode est plus efficace). Pour implémenter cette copie en temps linéaire et de manière à conserver le partage, il est utile d’ajouter aux références/variables un champs pointant éventuellement sur une copie de la référence. De plus il est souvent nécessaire de copier non pas un terme mais une structure (telle qu’une liste de termes) contenant des termes partageant certaines variables (ce qui permet d’automatiquement appliquer l’unificateur le plus général de deux termes u et v à tous les termes partageant les variables de u et/ou v). C’est pourquoi on propose une implémentation fonctionnelle de la copie permettant de traiter ce genre de cas (voir source).

Une implémentation purement fonctionnelle permettrait d’éviter ces copies. Mais dans ce cas la représentation de l’ensemble des équations serait moins efficace (un facteur log avec des map tables, ou un facteur linéaire si l’on utilise des vecteurs purement fonctionnel qu’il faut recopier à chaque modification).

L’implémentation qui suit propose aussi un algorithme de pattern-matching et un algorithme d’égalité restant linéaire. De plus l’algorithme de pattern-matching est optimisé pour anticiper certains échec en conservant pour chaque noeud du terme des informations pertinentes tel que la longueur ou la profondeur du terme. Cet algorithme est utilisé pour l’algorithme de résolution présenté dans la section suivante. En conséquence il est un peu alourdit par certain détails, et quelques fonctions présentes dans le source n’ont pas de rapports directs avec l’unification ellemême.

(* Type usuel rien ou objet *)
type 'a obj = Nothing | Something of 'a;;
(* Identificateurs des variables (utile uniquement pour l'affichage) *)
type var_info == int;;

(* Identificateurs des constantes (on distingue les prédicats et les fonctions)
     Les info. dans cst_info ne sont utilisés que pour l'affichage et le
     parsing. On utilise l'égalité physique pour comparer les symboles. *)
type cst_type = Pred_sym | Fun_sym;;
type cst_info = {Cst_name : string; Cst_arity : int; Cst_type : cst_type};;
(* Information sur les termes pour optimiser le pattern-matching *)
type Term_info = {mutable length : int;
                  mutable depth_max : int;
                  mutable depth_min : int};;
(* Representation des termes comme des graphes *)
type Term = {mutable Val : Value;
                mutable Dp : bool;
                mutable Ad : bool; (* Dp et Ad utilisés pour le test
                                   d'acyclicite *)
                mutable Copy : (Term_info * Term) obj (* Pour la copy *)}
and Value =
  Cst of (cst_info * Term vect * Term_info)
    (* Une constante appliquée à ces arguments *)
| Link of Term
    (* Le lien utilisé pour l'unification et le pattern-matching et
       exprimant que deux sous graphes doivent être égaux.*)
| Unknown of var_info
    (* Les variables *)
;;
(* L'exception levée en cas d'échec *)
exception Unif_fail;;
(* Le plus grand entier en Caml-Light *)
let max_int = 65536 * 16384 - 1;;
(* Construction du champs Term *)
let build v = {Val = v; Dp = false; Ad = false; Copy = Nothing};;
(* Génération de nouvelles variables *)
let count_var  = ref 0;;
let new_var () = let r = !count_var in count_var:=r+1; build (Unknown r);;
(* Un objet quelconque pour l'initialisation des vecteurs *)
let dummy = build (Unknown (-1));;
(* Suivi des liens et raccourcicement du chemin (la fonction G) *)
let rec getv modif t = fn t
  where rec fn t = match t.Val with
    Cst _| Unknown _-> t
  | Link t' ->
      let t'' = fn t' in
      if t' != t'' then (modif:=(t,t.Val)::!modif; t.Val <- Link t''); t''
;;
(* Suivi des liens sans raccourcicement du chemin (quand cela reste

   linéaire, il faut mieux utiliser getvs qui est "propre" *)
let rec getvs t = match t.Val with
  Cst _| Unknown _-> t
| Link t' -> getvs t'
;;
(* Généralisation de la fonction do_vect *)
let do_vect2 f v1 v2 =
  let n = vect_length v1 in
  for i = 0 to (n-1) do f v1.(i) v2.(i) done
;;
(* Fonction effectuant une liste de modifications pour "défaire" les
   modifications faites par unif, pmatch ou equal *)
let undo modif = do_list (function t,v -> t.Val <- v) modif;;
(* L'unification de termes rationnels. En cas d'echec les modifications
   sont "défaites" et l'exception Unif_fail est levée. En cas de réussite
   la liste des modifications est renvoyée. *)
let rec punif t1 t2 =
  let modif = ref [] in
  (try fn t1 t2; !modif
  with e -> undo !modif; raise e)
  where rec fn t1 t2 =
    let t1 = getv modif t1 and t2 = getv modif t2 in
    if t1 == t2 then () else
    match (t1.Val,t2.Val) with
      Cst (n1,v1,_), Cst (n2,v2,_) ->
        if n1 == n2 then begin
          modif:=(t1,t1.Val)::!modif;
          t1.Val <- Link t2; do_vect2 fn v1 v2
        end else
          raise Unif_fail
    | Unknown _, (Cst _| Unknown _) ->
        modif:=(t1,t1.Val)::!modif;
        t1.Val <- Link t2
    | Cst _, Unknown _->
        modif:=(t2,t2.Val)::!modif;
        t2.Val <- Link t1
    | _, _-> raise (Failure "bug: punif got link !")
;;
(* Test d'acyclicité avec nettoyage des champs Dp et Ad en cas de
   succès ou d'échec. Renvoie () : unit en cas de succès et lève
   Unif_fail sinon.  Le champs Ad est à true pour les variables qui
   sont sur le chemin de la racine à la position courante, tandis que
   Dp est à vrai pour les autres variables déjà testées. *)
let finite t = (try fn t; clean t with e -> clean t; raise e)
where rec fn t =
  let t = getvs t in
  if t.Ad then raise Unif_fail;
  if t.Dp then () else
    match t.Val with
      Cst(_,v,_) ->

      t.Ad <- true;
      do_vect fn v;
      t.Ad <- false;
      t.Dp <- true
  | _->
      t.Dp <- true
and clean t =
let t = getvs t in
if t.Dp or t.Ad then begin
  t.Dp <- false; t.Ad <- false;
  match t.Val with
    Cst(_,v,_) ->
      do_vect clean v
  | _-> ()
end
;;
(* L'unification complète elle-même. En cas d'echec les modifications
 sont "défaites" et l'exception Unif_fail est levée. En cas de réussite
 la liste des modifications est renvoyée. *)
let unif t t' =
let modif = punif t t' in
try
  finite t; modif
with e -> undo modif; raise e
;;
(* Suivi des liens et raccourcicement du chemin, de plus on renvoie
 un booléen pour dire si on a traversé un lien (utilisé par le pattern
 matching, car après avoir traversé un lien il est interdit de substituer
 les variables) *)
let getv' modif t =
match t.Val with
  Cst _| Unknown _-> t, false
| Link t' ->
    let t'' = getv modif t' in
    if t' != t'' then (modif:=(t,t.Val)::!modif; t.Val <- Link t'');
    (t'',true)
;;
(* Test de pattern-matching et d'égalité.
 Pour pmatch : En cas d'echec les modifications sont "défaites" et
   l'exception Unif_fail est levée. En cas de réussite la liste des
   modifications est renvoyée.
 Pour equal : Toujours propre, et renvoie un booléen *)
let pmatch,equal =
let b = ref false in
let modif = ref [] in
let rec fn lock t1 t2 =
let (t1,lock1) = getv' modif t1 and (t2,_) = getv' modif t2 in
let lock = lock or lock1 in
if t1 == t2 then () else
match (t1.Val,t2.Val) with
  Cst (n1,v1,i1), Cst (n2,v2,i2) ->

if n1 != n2 or
   i1.length > i2.length or
   i1.depth_max > i2.depth_max or
   i1.depth_min > i2.depth_min then
     raise Unif_fail;
modif:=(t1,t1.Val)::!modif;
t1.Val <- Link t2;
do_vect2 (fn lock) v1 v2
| Cst _, Unknown _->
raise Unif_fail
| Unknown _, _->
if lock then raise Unif_fail;
modif:=(t1,t1.Val)::!modif;
t1.Val <- Link t2;
b:= true
| _, _-> raise (Failure "bug: pmatch got link !")
in (fun t1 t2 -> b:= false; modif := [];
             try fn false t1 t2; (!b,!modif)
             with e -> undo !modif; raise e),
(fun t1 t2 -> b:= false; modif := [];
             try fn true t1 t2; undo !modif; true
             with Unif_fail -> undo !modif; false )
;;
(* fonction de copie d'une structure contenant des termes (les
fonctions fmap et fdo doivent être l'analogue de map et do_list
pour la structure concernée). La copie conserve le partage et
nettoie le champs Copy. Elle marche aussi sur des termes
cycliques. Les informations Term_info sont recalculées (car
l'argument provient en général du résultat d'une unification ou du
pattern-matching et ces informations ne sont en général plus
valable *)
let copy fmap fdo obj = (
let r = fmap fn obj in
(fdo clean obj : unit); r)
where rec fn t = let t = getvs t in
match t.Copy with
Something c -> c
| Nothing ->
match t.Val with
  Cst(f,v,_) ->
    let ni = {length = 1; depth_max = 0;
              depth_min = if vect_length v = 0 then 0 else max_int} in
    let nv = make_vect (vect_length v) dummy in
    (* La ligne suivante est à cette place pour autoriser la copie
       de termes cycliques *)
    let c = ni, build (Cst(f,nv,ni)) in t.Copy <- Something c;
    for i = 0 to (vect_length v) - 1 do
      let (ni',nt') = fn v.(i) in
      nv.(i) <- nt';
      ni.length <- ni.length + ni'.length;
      ni.depth_max <- max ni.depth_max (1 + ni'.depth_max);
      ni.depth_min <- min ni.depth_min (1 + ni'.depth_min)

        done;
        c
    | Unknown _->
        let ni = {length = 1; depth_max = 0; depth_min = 0} in
        let c = ni, new_var () in t.Copy <- Something c; c
    | _-> failwith "Bug: copy got link"
and clean t =
let t = getvs t in
if t.Copy = Nothing then () else begin
  t.Copy <- Nothing;
  match t.Val with
    Cst(_,v,_) ->
      do_vect clean v
  | _-> ()
end
;;
(* Les fonctions qui suivent sont utiles, mais n'ont pas de rapports
 directs avec l'unification. *)
(* fonction renvoyant une clef de hashage pour un terme. Cette clef
 satisfait : si equal t u = true alors key t = key u. On ne peut pas
 utiliser la fonction de hashage polymorphe de Caml-Light pour deux
 raisons :
   - La structure est cyclique.
   - L'égalité qui nous intéresse est "au nom des variables près".*)
let rec key t =
let hashval = ref 0 in
let dummy = {length = 0; depth_max = 0; depth_min = 0} in
let combine_small x = hashval := abs (!hashval * 7 + x)
and combine_big x = hashval := abs (!hashval * 65599 + x) in
let to_clean = ref [] in
let nv = ref 0 in
let nm = ref 75 in
let rec fn p t =
    let t = getvs t in
    match t.Val with
      Cst(f,v,_) ->
        combine_small 0;
combine_big (hashtbl__hash f.Cst_name);
        nm:=!nm-1;
        if !nm > 0 & p > 0 then do_vect (fn (p - 1)) v
    | Unknown n->
        nm:=!nm-1;
        let k = match t.Copy with
          Nothing ->
            nv:=!nv+1;
            t.Copy <- Something(dummy, build (Unknown !nv));
            to_clean:= t::!to_clean;
            !nv
        | Something(_, {Val = Unknown k}) -> k
        | _-> failwith "bug in key"
        in

        combine_small 1;
        combine_small k
    | _-> failwith "Bug: key got link"
in fn 10 t;
do_list (fun t -> t.Copy <- Nothing) !to_clean;
!hashval
;;
(* Affichage d'un terme, en utilisant le partage pour pouvoir afficher
 des gros termes ! La fonction do_print est un analogue fonctionnel
 (cf copie) permettant d'afficher une structure contenant des termes
 en visialisant le partage entre les différents termes. *)
let print_term, do_print =
let cur = ref 1 in
let dummy = {length = 0; depth_max = 0; depth_min = 0} in
let new_tag () = let r = !cur in
  cur:=r+1;
  Something (dummy, build (Unknown r))
and get_tag t = match t.Copy with
  Nothing -> raise Not_found
| Something (_,{Val = Unknown r}) -> "#"^(string_of_int r)
| _-> raise (Failure "bug 3 in print_term")
in
let rec fn t =
  let t = getvs t in
  match t.Val with
      Unknown r -> print_string "?"; print_string (string_of_int r)
    | Cst ({Cst_name = s},v,_) ->
        if v = [||] then print_string s else
        begin
          try
            let tag = get_tag t in
            print_string tag;
            if t.Dp then begin
              t.Dp <- false;
              print_string "=";
              raise Not_found
            end
          with Not_found ->
            print_string "(";print_string s;
            do_vect (fun t -> print_string " "; fn t) v;
            print_string ")"
        end
    | _-> raise (Failure "bug 1 in print_term")
and look_for_share t =
  let t = getvs t in
  match t.Val with
      Unknown _-> ()
    | Cst ({Cst_name = s},v,_) ->
        if v = [||] then () else
        if t.Dp then t.Copy <- new_tag ()
        else begin
          t.Dp <- true; do_vect look_for_share v

    end
| _-> raise (Failure "bug 2 in print_term")
and clean t =
let t = getvs t in
if t.Copy = Nothing & not t.Dp then () else begin
t.Copy <- Nothing;
t.Dp <- false;
match t.Val with
  Cst(_,v,_) ->
    do_vect clean v
| _-> ()
end
in
(fun t -> cur:=1; look_for_share t; fn t; clean t),
(fun (g : (Term -> unit) -> Term list * Term list -> unit)
 (h : (Term -> unit) -> Term list * Term list -> unit) o ->
cur:=1; g look_for_share o; h fn o; g clean o)
;;
(* Lecture des informations sur les termes *)
let get_info t = match (getvs t).Val with
Unknown _-> {length = 1; depth_max = 0; depth_min = 0}
| Cst(_,_,i) -> i
| _-> failwith "Bug in get_info"
;;
(* Construction d'une application avec calcul des informations
(utilisé par le parser pour construire des termes. *)
let build_app f l =
let len = list_length l in
let nv = make_vect len dummy in
let ni = {length = 1; depth_max = 0;
      depth_min = if len = 0 then 0 else max_int} in
let i = ref 0 in
do_list (
fun t ->
let ni' = get_info t in
ni.length <- ni.length + ni'.length;
ni.depth_max <- max ni.depth_max (1 + ni'.depth_max);
ni.depth_min <- min ni.depth_min (1 + ni'.depth_min);
nv.(!i) <- t;
i:=!i+1)
l;
build (Cst(f,nv,ni))
;;

4 La résolution en calcul des prédicats.

4.1 La résolution binaire.

En plus des constantes de fonctions et des variables déjà utilisées pour définir les termes, on se donne un ensemble de symboles de prédicat d’arités diverses. On définit alors les notions suivantes :

– P (t_{1}, …, t_{n}) est une formule atomique si P est un symbole de prédicat d’arité n et si t_{1}, …, t_{n} sont des termes.

– A et ¬A sont des littéraux si A est une formule atomique. On dira que A est un littéral positif et que ¬A est un littéral négatif.

– Une clause est un ensemble de littéraux, notée ∅ pour la clause vide et L_{1}, …, L_{n} sinon. On peut étendre les notions d’unification et de pattern-matching aux littéraux. On notera

mgu(L, K) l’unificateur le plus général des littéraux L et K. De plus on notera \overline{L} la négation du littéral L (si L est égal à la formule atomique A, \overline{L} = ¬A, et si L est égal à ¬A, \overline{L} = A).

On peut maintenant définir les deux règles de dérivations suivantes :

– La résolution L_{0}, L_{1}, …, L_{n} K_{0}, K_{1}, …, K_{m}

σ = mgu(L_{0}, \overline{K_{0}})
σL_{1}, …, σL_{n}, σK_{1}, …, σK_{m}

– La contraction

L_{0}, L_{1}, …, L_{n}
σ = mgu(L_{0}, L_{1})
σL_{1}, …, σL_{n}

On peut alors voir un ensemble de clause comme une théorie contenant l’ensemble des formules du calcul des prédicats construites en quantifiant universellement la disjonction des littéraux contenus dans une clause. On peut prouver que cette théorie est insatisfaisable (on contradictoire) si et seulement si l’on peut dériver la clause vide à partir des clauses initiales en utilisant les deux règles ci-dessus. Ceci peut être formalisé de la manière suivante : Si C_{0} est un ensemble de clauses, on définit

– R(C) l’ensemble des clauses obtenues par application de la règle de résolution à deux clauses de C

– C(C) l’ensemble des clauses obtenues par une ou plusieurs application de la règle de contraction à une clause de C.

– C_{n+1} = C ∘ R(C_{n}) ∪ C_{n}

Alors, C_{0} correspond à une théorie contradictoire si et seulement si il existe n tel que ∅ ∈ C_{n}. Cette technique de résolution s’appelle la résolution binaire car la règle de résolution est appli-

quée à toutes les paires de clauses. Cette méthode, bien que complète, est impraticable sauf sur des exemples très simples. Afin de l’améliorer, il faut considérer des optimisations tel que l’élimination des tautologies ou la subsumption (section 4.2) et des stratégies (section 4.3).

Une première optimisation, est l’élimination des tautologies. En effet, des clauses qui contiennent un littéral et sa négation sont des tautologies et ne peuvent être utile pour rechercher une contradiction. Elle peuvent donc ne pas être prises en considération.

4.2 La subsumption.

La subsumption permet d’éliminer de nombreuses clauses conséquences immédiates d’une autre clause. Elle peut être définit de la manière suivante : Une clause C = L_{1}, …, L_{n} subsume une clause C′ si et seulement si il existe une substitution σ tel que σC = σL_{1}, …, σL_{n} ⊆ C′.

On peut tout en conservant la complétude éliminer à chaque étape de résolution toutes clauses qui est subsumées par une autre. On distingue alors la “forward subsumption”, lorsque qu’une clause nouvelle n’est pas retenu car elle est subsumée par une ancienne clause, et la “backward subsumption” lorsqu’une ancienne clause est éliminée car subsumée par une clause nouvelle.

Il faut noter que la règle de contraction est nécessaire pour le complétude. De plus, en présence de la subsumption, elle permet de considérer les clauses aussi bien comme des ensembles ou des multi-ensembles, puisqu’une clause contenant deux fois le même littéral est contracté en une clause qui subsume la clause de départ.

Cette procédure de subsumption est essentielle et permet d’éliminer un grand nombre de clauses. Toutefois, cela reste très insuffisant et l’on doit utiliser des stratégies permettant de réduire encore le nombre de clauses considérées.

4.3 “Set of support” et Hyper-résolution.

Les stratégies dites “Set of support” sont des stratégies “sémantiques”. On considère un modèle M, et l’on va considérer la restriction qui consiste à n’ajouter que des formules qui ne sont pas valides dans ce modèle.

Ainsi on définit la M-résolution de la manière suivante : On considère une clause C_{0} tel que M ⊧ C_{0} et un ensemble de clauses S tel que pour toutes clauses D ∈ S, M |̸= D. S’il existe des clauses C_{1}, …, C_{n} tel que C_{i+1} soit obtenue par application de la règle de résolution à C_{i} et D_{i} ∈ S et si M |̸= C_{n}, alors C_{n} est un M-résolvant de C_{O} et D_{0}, …, D_{n−1}.

L’Hyper-résolution est le cas particulier on l’on prend le modèle M tel que pour toutes constantes de prédicat P d’arité n et tous termes t_{1}, …, t_{n} on a M ⊧ ¬P (t_{1}, …, t_{n}). L’hyperrésolution ne produit donc que des clauses contenant des littéraux positifs. En effet, pour obtenir un nouvel hyper-resolvant, on part d’une clause contenant au moins un littéral négatif et on applique la règle de résolution avec des clauses ne contenant que des littéraux positifs jusqu’à avoir éliminer tous les littéraux négatifs.

De manière analogue, on peut définir l’hyper-résolution négative en échangeant le rôle des littéraux positifs et négatifs.

L’avantage de ce type de stratégie est que peu de clauses sont conservées (toutes les clauses intermédiaires sont éliminées), ce qui facilite la subsumption. De plus ce type de stratégies simplifie la contraction car elle n’est pas nécessaire sur les clauses intermédiaires. De plus on peut ne pas contracter les littéraux valides dans le modèle (les littéraux négatifs dans le cas de l’hyperrésolution) et conserver la complétude.

4.4 Mise sous forme clausale.

Afin de rechercher si une formule du calcul des prédicats est prouvable en utilisant la méthode de résolution, il faut la mettre sous formes d’un ensemble de clauses qui sera contradictoire si et seulement si la formule originale est prouvable.

Pour cela, il suffit de considérer la négation de la formule et d’appliquer les étapes suivantes :

– Descendre les négations au niveau atomique afin que toutes les sous-formules non atomiques apparaissent positivement (il faut donc remplacer l’implication et l’équivalence par leur définition en terme de conjonctions, disjonctions et négations).

– Éliminer les quantificateurs existentiels par la skolémisation. Si une sous-formule de la forme ∃xF apparaît, on peut la remplacer par F [x ← f(x_{1}, …, x_{n})] où x_{1}, …, x_{n} sont les variables de F quantifiées universellement.

– Amener tous les quantificateurs universels en tête de la formule (mise sous forme prénexe).

– Utiliser les règles de distributivité de la conjonction et de la disjonction pour mettre la formule sous forme de clauses.

Note : il est important de faire la skolémisation avant la mise sous forme prénexe pour éviter d’introduire des constantes de fonctions d’arité inutilement grande. De plus, si la formule de départ est une conjonction de plusieurs formules, il vaut mieux prouver chaque terme de la conjonction séparément (cela évite d’avoir trop de clauses). Une autre optimisation (non implémentée) consiste à utiliser la subsumption et d’autres transformations au fur et à mesure de la construction de l’ensemble des clauses afin de limiter encore leur nombre.

4.5 Implémentation.

L’hyper-résolution est une des stratégies les plus efficaces. Toutefois, entre la présentation formelle de la résolution que l’on vient de décrire et une implémentation efficace, il y a une marge assez importante. Il faut absolument tenir compte des points suivants :

– Les clauses unitaires (et de manière moindre les petites clauses) doivent être privilégier.

– La subsumption doit être efficace ce qui requiert pas mal de “truc”. L’implémentation cidessous n’est pas parfaite sur ce point. En particulier, le cas de la résolution pas les clauses unitaires peut être traiter séparément de manière plus efficace (ce qui n’est pas fait dans ce qui suit).

– La contraction doit être implémentée avec précaution pour éviter de produire un grand nombre de fois les mêmes clauses (cf source).

– La règle d’hyper-résolution nécessite de résoudre sur le littéral négatif offrant le moins de possibilités en premier pour éviter une recherche catastrophique des hyper-résolvants (cf. source). Il serait par exemple ridicule de résoudre une clause contenant un littéral négatif qui ne s’unifie avec aucun littéral positif !

(* on a besoin de l'unification linéaire .... *)
#open "unif";;
(* les trois stratégies implémentées *)
type strategie = Binary | Hyper | NegHyper;;
(* type des termes (sous forme d'arbre et nom sous forme de graphe
   comme pour l'unification linéaire), utilisé uniquement avant la
   mise sous forme de clauses *)
type term =
  Fun of (cst_info * term list)
| BVar of int (* indice de De Bruijn de la variable *)
;;
(* type des prédicats du premier ordre *)
type prop =
  Vrai | Faux
| Atom of term
| Et of prop * prop
| Ou of prop * prop
| Im of prop * prop
| Eq of prop * prop
| Non of prop
| Al of prop
| Ex of prop
;;
(* type des informations ajoutées aux clauses pour optimiser la subsumption
     nb de lit. pos., nb de lit. neg.,
     longueur total des lit. pos.,
     max depth dans lit. pos., min depth dans lit pos.,
     idem des trois derniers pour lit neg *)
type info ==
  int * int * int * int * int * int * int * int
;;
(* type des clauses:
     numero de la clause,
     True pour les clauses initiale,
     info (cf ci-dessus),
     liste des lit. pos., listes lit. nég *)
type clause ==
  int ref * bool * info * Term list * Term list
;;

(* Génération de nouvelles constantes de fonctions *)
let count_cst = ref 0;;
(* Cette fonction est appelé par la skolémisation uniquement, l'arité et
   le nom n'ont donc pas d'importance. *)
let new_cst () =
  let r = !count_cst in count_cst:=r+1;
  {Cst_name = "!"^(string_of_int r); Cst_arity = 0; Cst_type = Fun_sym};;
(* Remise à zero des compteurs *)
let reset_ref () =
  count_var := 0; count_cst := 0;;
(* n-ième élt. d'une liste *)
let rec nth = fun
  0 (a::_) -> a
| n (_::l) -> nth (n-1) l
| __-> raise (Invalid_argument "nth")
;;
(* deux exceptions *)
exception Fail;;
exception Proved;;
(* transforme une formule en une liste de formules dont la conjonction est
   équivalente à la formule de départ. *)
let rec devl p =
  let rec fn pos = function
  Et(p,p') as p'' -> if pos then fn pos p @ fn pos p' else [Non p'']
| Ou(p,p') as p'' -> if pos then [p''] else fn pos p @ fn pos p'
| Im(p,p') as p'' -> if pos then [p''] else fn (not pos) p @ fn pos p'
| Eq(p,p') as p'' -> if pos then fn pos (Et (Ou (Non p,p'), Ou (p,Non p')))
                     else fn pos (Ou (Et (p,p'), Et (Non p,Non p')))
| Non p -> fn (not pos) p
| Al p as p' -> if pos then map (fun x -> Al x) (fn pos p) else [Non p']
| Ex p as p'-> if pos then [p'] else map (fun x -> Al x) (fn pos p)
| Atom _as p -> if pos then [p] else [Non p]
| Vrai -> if pos then [] else raise Fail
| Faux -> if pos then raise Fail else []
  in fn true p
;;

(* transformation d'un prédicat en un ensemble de clauses *)
let prop_clause p =
  let rec fn pos env =
    let rec do_sk p = function
      true -> let v = new_var () in fn pos (v::env) p
    | false -> let n = new_cst () in fn pos ((build_app n (uvars env p))::env) p
    and join (lp,ln) (lp',ln') = (union lp lp') ,(union ln ln')
    and uvars env f = (gn 0 p
      where rec gn d = function
        Al p -> gn (d+1) p

    | Ex p -> gn (d+1) p
    | Atom t -> hn t
       where rec hn = (function
         BVar n -> if n < d then []
                   else let t = nth (n-d) env in
                   (match t.Val with Unknown _-> [t] | _-> [])
       | Fun (_,l) -> flat_map hn l)
    | Et (p,p') -> union (gn d p) (gn d p')
    | Ou (p,p') -> union (gn d p) (gn d p')
    | Im (p,p') -> union (gn d p) (gn d p')
    | Eq (p,p') -> union (gn d p) (gn d p')
    | Non p -> gn d p
    | Vrai | Faux -> [])
  and do_clause pos p pos' p' = function
    true -> union (fn pos env p) (fn pos' env p')
  | false ->  (try let l = fn pos env p in
                  try let l' = fn pos' env p' in
                    it_list (fun res cl -> union res (map (join cl) l')) [] l
                  with Proved -> l
                with Proved -> fn pos' env p')
  in function
  Al p -> do_sk p pos
| Ex p -> do_sk p (not pos)
| Atom t ->
  let rec fn = function
    BVar n -> nth n env
  | Fun (n,l) -> build_app n (map fn l)
  in let t = fn t in if pos then [[t],[]] else [[],[t]]
| Et (p,p') -> do_clause pos p pos p' pos
| Ou (p,p') -> do_clause pos p pos p' (not pos)
| Im (p,p') -> do_clause (not pos) p pos p' (not pos)
| Eq (p,p') -> if pos then
                 fn pos env (Et (Ou (Non p,p'), Ou (p,Non p')))
               else
                 fn pos env (Ou (Et (p,p'), Et (Non p,Non p')))
| Non p -> fn (not pos) env p
| Vrai -> if pos then [] else raise Proved
| Faux -> if pos then raise Proved else []
in fn true [] p
;;
(* affichage d'une clause *)
let print_clause (n,_,_,l1,l2) =
print_char `<`; print_int !n; print_char `>`;
let g f (l1,l2) = do_list f l1; do_list f l2
and h f (l1,l2) =
  if l1 = [] & l2 = [] then print_string " []";
  do_list (fun t -> print_string " ~"; f t) l2;
  do_list (fun t -> print_string " "; f t) l1
in
do_print g h (l1,l2);

  print_newline ()
;;
(* comparaison des infos d'une clause *)
let compare_info
  (l1,l2,a1,a2,a3,a4,a5,a6) (l1',l2',a1',a2',a3',a4',a5',a6') =
  l1 > l1' or l2 > l2' or a1 > a1' or a2 > a2' or a3 > a3' or a4 > a4'
  or a5 > a5' or a6 > a6'
;;
(* doit-on afficher des informations pendant la résolution *)
let verbose = ref false;;
(* Quelle stratégie *)
let strategie = ref Hyper;;
(* la liste des axiomes (conservés pour plusieurs résolution). *)
let axiom = ref ([] : (Term list * Term list) list);;
(* la table des clauses, la clef entière donne la "génération" de la clause *)
let clauses = (myhashtbl__new 23 myhashtbl__Standard myhashtbl__Standard
                  : (int,clause list) myhashtbl__t);;
(* génération courante (en train d'être résolue avec les générations
   plus récentes) *)
let cur_gen = ref 1;;
(* génération maximum contenant au moins une clause *)
let max_gen = ref 0;;
(* fabrication des numéros des clauses *)
let cur = ref 1;;
let new () = let r = !cur in cur := r + 1; ref r;;
(* fabrication des informations sur une liste de litéraux *)
let linfo l =
  it_list (fun (a1,a2,a3) t ->
    let ni = get_info t in
    (a1+ni.length,max a2 ni.depth_max,max a3 ni.depth_min))
  (0,0,0) l
;;
(* généralisation de map et do_list aux paires de listes *)
let map_pair fn (lp,ln) =
  let fn = fun x -> snd (fn x) in
  (map fn lp, map fn ln);;
let do_pair fn (lp,ln) = do_list fn lp; do_list fn ln;;
(* fabrication d'une nouvelle clause (avec copie des termes !) *)
let build_clause ax lp ln =
  let (lp,ln) = copy map_pair do_pair (lp,ln) in
  let (a1,a2,a3) = linfo lp and (a4,a5,a6) = linfo ln in
  let info = (list_length lp,list_length ln,a1,a2,a3,a4,a5,a6) in
  (new (),ax,info,lp,ln)

;;
(* copie d'une clause*)
let copy_clause (r,ax,info,lp,ln) =
  let (lp,ln) = copy map_pair do_pair (lp,ln) in
  (r,ax,info,lp,ln)
;;
(* application d'une fonction à toutes les clauses *)
let it_clauses f a =
  myhashtbl__it_table (fun a _l -> it_list f a l) a clauses;;
(* test des tautologies *)
let tautologie lp ln =
  exists (fun c -> exists (fun c' -> equal c c') ln) lp;;
(* algorithme de subsumption *)
let subsume (no,_,i,lp,ln) (no',_,i',lp',ln') =
  let rec fn = fun
    [] [] -> ()
  | [] (t::ln) -> hn t [] ln ln'
  | (t::lp) ln -> hn t lp ln lp'
  and hn t lp ln = function
    [] -> raise Fail
  | t'::l' -> try
                let b, modif = pmatch t t' in
                try
                  fn lp ln; undo modif
                with Fail -> undo modif; if b then hn t lp ln l' else raise Fail
              with Unif_fail -> hn t lp ln l'
  in
  if (compare_info i i') then false else
  try
    fn lp ln;
    if !verbose then begin
      print_string "clause ";
      print_int !no';
      print_string " subsumed by ";
      print_int !no;
      print_newline ()
    end;
    true
  with Fail -> false
;;
(* un type d'arbre utilisé pour la contraction *)
type 'a tree = N of 'a * 'a tree ref list ref | D
;;
(* trois fonctions auxilliaire pour la contraction *)
let delete a b =
  let rec fn t =
    if t == a then b:=!a
    else match t with

    ref D -> ()
  | ref (N (cl,ptr)) as p -> p:=D; do_list fn !ptr
in fn b; if !b == !a then raise Exit
;;
let exists_in_tree t f = fn t
where rec fn = function
  ref D -> false
| ref (N (cl,ptr)) -> if f cl then true else exists fn !ptr
;;
let tree_to_list t = fn [] t
where rec fn acc = function
  ref D -> acc
| ref (N (cl,ptr)) -> it_list fn (cl::acc) !ptr
;;
(* la contraction *)
let contract (_,ax,_,_,_as cl) =
let tree = ref (N (cl, ref [])) in
let to_do = ref [tree] in
begin
  while !to_do <> [] do
    match !to_do with
      [] -> ()
    | t::l -> to_do := l; contract_one t
  done;
  tree_to_list tree
end
where rec contract_one = function
  ref D -> ()
| ref (N (no,_,_,lp,ln as cl, ptr)) as curptr ->
    let rec fn lp' ln' lp ln =
      let rec hn t lp ln = function
        [] -> ()
      | t'::l' ->
          (try
            let modif = unif t t' in
            let lp'',ln'' = copy map_pair do_pair (lp,ln) in
            undo modif;
            if tautologie lp'' ln'' then () else (
            let cl = build_clause ax lp'' ln'' in
            if !verbose then begin
              print_string "clause ";
              print_int !no;
              print_string " contract to ";
              print_clause cl
            end;
            if it_clauses (fun b c' -> b or (subsume c' cl)) false
              then () else (
            if exists_in_tree tree (function c -> subsume c cl)
              then () else (

          let ptrn = ref (N (cl, ref [])) in
          ptr:= ptrn :: !ptr;
          let rec kn = function
            ref D -> ()
          | ref (N (cl',ptr)) as ptro ->
              if subsume cl cl' then delete ptrn ptro
          in kn tree)))
        with Unif_fail -> ()); hn t lp ln l'
    in match lp,ln with
    [], [] -> ()
  | [], (t::ln) -> hn t lp' (ln'@ln) ln; fn lp' (t::ln') [] ln
  | (t::lp), ln -> hn t (lp'@lp) (ln'@ln) lp; fn (t::lp') ln' lp ln

in try fn [] [] lp ln with Exit -> ();
let ncl = !ptr in
if ncl <> [] then to_do := !to_do @ ncl
;;
(* la résolution, les litéraux t et t' à résoudre on été retirés des clauses
données en second et quatrième argument.
 teste pour les tautologies et la forward subsumption  *)
let rec resolve t (no,_,_,lp',ln') t' (no',_,_,lp'',ln'') =
if !no < 0 or !no' < 0  then [] else
try
let modif = unif t t' in
let lp = lp'@lp'' and ln = ln'@ln'' in
let ((_,_,_,lp,ln) as cl) = build_clause false lp ln in
undo modif;
if !verbose then begin
  print_string "res ";
  print_int !no;
  print_char ` `;
  print_int !no';
  print_string " gives ";
  print_clause cl
end;
if lp = [] & ln = [] then raise Proved;
if tautologie lp ln then [] else
if it_clauses (fun b c' -> b or (subsume c' cl))
       false then []
else [cl]
with Unif_fail -> []
;;
(* ajout d'une clause dans la table des clauses.
  appel la contraction et effectue la backward subsumption *)
let add_clause nc =
let nc = contract nc in
myhashtbl__do_table (fun n l ->
let nl = it_list (fun ng c ->
if (exists (fun c' -> subsume c' c) nc) then
  (let (no,_,_,_,_) = c in no:= -1;ng) else c::ng) [] l in
myhashtbl__remove clauses n;

    myhashtbl__add clauses n nl) clauses;
  do_list (fun ((no,_,(i,j,_,a2,a3,_,a5,a6),lp,ln) as c) ->
    if !verbose then begin
      print_string "keep clause "; print_int !no; print_newline ()
    end;
    let gen = (i + j) * (a2 + a5 + 1) + !cur_gen in
    if gen > !max_gen then max_gen := gen;
    let old =
      try
        let l = myhashtbl__find clauses gen in
        myhashtbl__remove clauses gen; l
      with Not_found -> []
    in myhashtbl__add clauses gen (c::old)) nc
;;
(* teste si une clause est unitaire *)
let unit (_,_,_,lp,ln) = (fun
  [] [_] -> true
| [_] [] -> true
| __-> false) lp ln
;;
(* teste suivant la stratégie si une clause doit être ajoutée.
   Dans le cas des set-of-support strategy, les clauses unitaires sont
   toujours ajoutées. *)
let rec add_new = function
  [] -> []
| (no,ax,i,lp,ln as cl)::l ->
    if !strategie = Binary or (!strategie = Hyper & ln = [])
                           or (!strategie = NegHyper & lp = []) then begin
      add_clause cl;
      add_new l
    end else begin
      if unit cl then add_clause cl;
      cl::(add_new l)
    end
;;
(* table indiquant le nombre de possibilité d'unification d'un
   litéral.  Cela permet de ne pas calculer plusieurs fois cette
   valeur. Cette table est effacée à chaque nouvelle génération *)
let pondt = myhashtbl__new 401 (myhashtbl__Custom key)
                               (myhashtbl__Custom equal);;
(* fonction recherchant l'élément minimum d'une liste *)
let min_first cmp l =
  let rec fn m acc = function
    x::l -> if cmp x m then fn x (m::acc) l else fn m (x::acc) l
  | [] -> m::acc
  in match l with
    [] -> []
  | x::l -> fn x [] l
;;

(* trie les litéraux d'une liste pour placer en premier le litéral
ayant le moins d'unification possible *)
let sort_lit  l =
let pondere lit =
let c = ref 0 in
let rec fn = function
  [] -> ()
| t::l ->
  (try let modif = unif t lit in c:=!c+1; undo modif
  with Unif_fail -> ());
  fn l
in
let gn (no,_,_,lp,ln) = if !no > 0 then (
                       if !strategie = Hyper then
                         if ln = [] then fn lp else ()
                       else if !strategie = NegHyper then
                         if lp = [] then fn ln else ()
                       else ())
in
for i = 1 to !cur_gen do
  try
    let cur = myhashtbl__find clauses i in
    do_list gn cur
  with Not_found -> ()
done;
!c
in
let hpond lit = myhashtbl__add_find pondt lit pondere in
let l = map (fun x -> hpond x, x) l in
let l = min_first (fun x y -> fst x <= fst y) l in
if fst (hd l) = 0 then raise Exit;
map snd l
;;
(* calcule toutes les résolutions possible de deux clauses suivant la
stratégie.  le booléen donné en premier argument permet de
distinguer l'appel initial des appels récursifs (inutile pour la
résolution binaire). *)
let rec resolve_all ft (no,ax,i,lp,ln) (no',ax',i',lp',ln') =
if !no > 0 & !no' > 0 &
 ((!strategie = Binary) or
 (!strategie = Hyper & ln = []) or
 (!strategie = NegHyper & lp' = [])) then
let rec fn lp0 = function
[] -> ()
| p::lp -> gn p (lp0@lp) [] ln';
         if !strategie <> NegHyper or ft then fn (p::lp0) lp
and gn p lp ln0' = function
[] -> ()
| n::ln' ->
let nc = resolve p (no,ax,i,lp,ln) n (no',ax',i',lp',(ln0'@ln')) in
let nc = add_new nc in

    let rec kn acc = function
      [] -> acc
    | (no,ax,i,lp,ln as cl)::l ->
        try match !strategie with
          Binary -> failwith "bug in resolve all"
        | Hyper -> if list_length ln > 1
                   then kn ((no,ax,i,lp,sort_lit ln)::acc) l
                   else kn (cl::acc) l
        | NegHyper ->
                   if list_length lp > 1
                   then kn ((no,ax,i,sort_lit lp,ln)::acc) l
                   else kn (cl::acc) l
        with Exit -> kn acc l
    in
    let nc = kn [] nc in
    if nc <> [] then myhashtbl__do_table
      (fun g cur -> if g <= !cur_gen then do_next_sgen false nc cur)
      clauses;
    if !strategie <> Hyper or ft then gn p lp (n::ln0') ln'
  in fn [] lp
(* Fonction testant toutes les résolutions possibles à l'intérieur
   d'une liste de clauses *)
and do_next_gen = fun
  [] -> ()
| (cur::l) ->
     resolve_all true cur (copy_clause cur);
     do_list (fun cur' -> resolve_all true cur cur';
                          resolve_all true cur' cur) l;
     do_next_gen l
(* Fonction testant toutes les résolutions possibles entre deux listes
   de clauses *)
and do_next_sgen ft = fun
  [] _-> ()
| (cur::l) l' ->
     do_list (fun cur' -> resolve_all ft cur cur';
                          resolve_all ft cur' cur) l';
     do_next_sgen ft l l'
;;
(* fonction d'initialisation *)
let do_init typ = myhashtbl__clear clauses; cur := 1;
                 cur_gen := 0; max_gen := 0;
                 strategie := typ;
                 reset_ref ();
                 do_list (function lp,ln ->
                          if not tautologie lp ln then begin
                            let cl = build_clause true lp ln in
                            if !verbose then print_clause cl;
                            if not (it_clauses
                                      (fun b c' -> b or (subsume c' cl))
                                       false)

                            then add_clause cl
                            end) !axiom
;;
(* fonction ajoutant un axiome *)
let addax prop =
  let first = prop_clause prop in
  axiom := first@(!axiom)
;;

(* fonction effectuant la résolution (le premier argument étant la
   stratégie et le second la formule à prouver) *)
let oneres typ prop =
  do_init typ;
  let first = prop_clause (Non prop) in
  do_list (function lp,ln ->
             if not tautologie lp ln then begin
               let cl = build_clause true lp ln in
               if !verbose then print_clause cl;
               if not (it_clauses
                         (fun b c' -> b or (subsume c' cl))
                         false)
               then add_clause cl
               end) first;
  cur_gen := 1;
  try
    while true do
      if !strategie <> Binary then myhashtbl__clear pondt;
      (try let new = myhashtbl__find clauses !cur_gen in
      if !verbose then print_endline "starting new generation.";
      let rec fn n =
        if n = !cur_gen then do_next_gen new
        else (
          (try let old = myhashtbl__find clauses n in
            do_next_sgen true new old
          with Not_found -> ());
          fn (n+1)) in
      fn 1
      with Not_found -> ());
      cur_gen:=!cur_gen+1;
      if !cur_gen > !max_gen then raise Fail
    done; true
  with Proved -> true | Fail -> false
;;
(* fonction appelant la fonction "devl" puis la résolution sur chacune des
   formules *)
let res typ prop =
  for_all (oneres typ) (devl prop)
;;

A Générateur aléatoire de formules.

Le code suivant définit une fonction random_form n p construisant aléatoirement une formule de longueur n utilisant p variables.

(* générateur aléatoire de formules *)
(* transforme une liste en un arbre binaire en utilisant la fonction conn
   pour construire les noeuds de l'arbre *)
let rec make_bin conn = function
    [a] -> a
  | a::l -> conn a (make_bin conn l)
  | _-> failwith "bug in make_bin"
;;
(* fabrique nc clauses de longueur lc utilisant nv variables *)
let random_clause nv nc lc =
  let rec fn l = function
0 -> l
  | n -> let v = random__int nv and b = (random__int 2 = 1) in
         if exists (fun (_,v') -> v = v') l then fn l n else fn ((b,v)::l) (n-1)
  and gn l = function
    0 -> l
  | n -> gn ((fn [] lc)::l) (n-1)
  in gn [] nc
;;
(* transforme une liste de clauses en une disjonction de conjonctions *)
let clause_to_form neg cl =
  make_bin (fun x y -> Bin((if neg then Ou else Et),x,y))
    (map (fun l ->
      make_bin (fun x y -> Bin((if neg then Et else Ou),x,y))
        (map (function b,n -> if neg <> b then Var n else Non (Var n)) l)) cl)
;;
(* générateur aléatoire de formules *)
let random_form tt n p = clause_to_form true (random_clause tt n p);;

B Un chronomètre

Le petit programme suivant chronomètre le temps nécessaire pour appliquer une fonction à un argument (le temps de calcul de l’argument n’étant pas compris).

(* Le petit programme suivant chronomètre le temps nécessaire pour

appliquer une fonction à un argument (le temps de calcul de l'argument
n'étant pas compris). *)
(* necessite la librairie UNIX *)
let chrono f x =
let {unix__tms_utime = ut;unix__tms_stime = st} = unix__times () in
let r = f x in
let {unix__tms_utime = ut';unix__tms_stime = st'} = unix__times () in
printf__printf "Time = %fs of S+U time\n" ((ut' -. ut) +. (st' -. st));
r
;;

C Utilisation du démonstrateur de théorèmes.

Avec les exemples, sur ftp, une interface est fournie pour le démonstrateur de théorèmes en résolution.

Voici la liste des commandes :

– cst f n ; définit une constante de fonction f d’arité n.

– pred p n ; définit une constante de prédicat p d’arité n.

– axiom F ; ajoute la formule F à la liste des axiomes.

– reset; efface toutes les déclarations de symboles de fonction ou de prédicat ainsi que les axiomes.

– bres F ; essaye de prouver F en utilisant la résolution binaire.

– hres F ; essaye de prouver F en utilisant l’hyper-résolution.

– nhres F ; essaye de prouver F en utilisant l’hyper-résolution négative.

– (* .... *) permet d’insérer des commentaires.

– include "nomdefichier"; lit le fichier “nomdefichier.pred”.

– quit; ... devinez. Tous les identificateurs alphanumériques ne commençant pas par un chiffre sont admis pour les

variables et les constantes. Les caractères “'” et “_” peuvent aussi être utilisés (cf. les identificateurs du module genlex de Caml-Light).

La syntaxe des formules est la suivantes :

– Un identificateur non déclaré est une variable du premier ordre.

– Si f est une constante de fonction d’arité n, et si e1, …, en sont n expressions désignant des termes, f e1 ... en désigne l’application du symboles de fonction aux termes, le résultat étant lui-même un terme.

– Si p est une constante de prédicat d’arité n, et si e1, …, en sont n expressions désignant des termes, f e1 ... en désigne l’application du symboles de prédicat aux termes, le résultat étant lui-même une formule.

– F & G désigne une conjonction.

– F or G désigne une disjonction.

– F -> G désigne une implication.

– F <-> G désigne une équivalence.

– ~ F désigne la négation.

– Al x F désigne la quantification universelle.

– Ex x F désigne la quantification existentielle.

– Les priorité sont, par ordre croissant : Al,Ex < & < or < -> < <->.

– Les parenthèses peuvent être utiliser pour grouper des expressions.

Exemple :

cst e 0;
cst i 1;
cst mul 2;
pred eq 2;
axiom Al x eq x x;
axiom Al x Al y (eq x y -> eq y x);
axiom Al x Al y Al z (eq x y -> eq y z -> eq x z);
axiom Al x Al y (eq x y -> eq (i x) (i y));
axiom Al x Al y Al z Al t (eq x y -> eq z t -> eq (mul x z) (mul y t));
axiom Al x Al y Al z eq (mul x (mul y z)) (mul (mul x y) z);
axiom Al x eq (mul x e) x;
axiom Al x eq (mul x (i x)) e;
nhres Al x eq (mul e x) x;

Note :cet exemple n’est pas résolu en plusieurs heures sur une station Sparc 10.