Tableaux à variables libres

2 Tableaux à variables libres

2.1 Présentation

Une amélioration de la méthode des tableaux de base que nous avons présentée en section 1 est la méthode des tableaux à variables libres, comme Melvin Fitting l'appelle [Fit83].

g-règles

g g₁

+$ x· F +F[x'/x]

-" x· F -F[x'/x]

(où x' est une nouvelle variable)

Figure 2: g-règles en tableaux à variables libres

Dans les tableaux à variables libres, les étapes d'extension sont intégrées dans le processus de recherche de preuve lui-même, en utilisant des versions paresseuses des règles $R et "L de LK, de la même façon que l'on pouvait expliquer la résolution en termes d'une règle de coupure paresseuse. Ces règles sont :

où x' est une nouvelle variable, qui représente le terme t dans la règle correspondante de LK. Nous avons vu que, au lieu de deviner t, la méthode des tableaux le calculait en liant x' à t lors du calcul d'un unificateur servant à clore un chemin (de façon équivalente, pour faire du séquent une instance de Ax). Ceci se traduit en ce qu'on appelle les g-règles de la méthode des tableaux à variables libres : voir la figure 2.

Nous pouvons aussi adapter les règles "R et $L, de sorte qu'il ne sera pas nécessaire d'herbrandiser la formule à prouver dans une étape de pré-traitement. Une façon de la faire est d'introduire de nouvelles versions de "R et $L, du style des règles ci-dessus, mais soumises à la condition que la variable nouvellement introduite x' ne doit pas être liée à aucun terme pendant l'unification. Nous pouvons faire respecter cette condition en créant une nouvelle constante plutôt qu'une nouvelle variable. Ceci mène aux règles suivantes :

où c est une nouvelle constante.

Ceci ne suffit pas encore, cependant, parce que nous devons être sûrs non seulement que c n'apparaît pas dans G ni dans D, mais ausi qu'elle n'apparaitra dans aucune instance de G et D que nous produirons jamais par unification. Considérons en effet le séquent :

¾® $ x · " y · P (x, y) Þ P (y, x)

qui n'est pas valide : prendre pour P la relation £ sur les entiers, par exemple. Si l'on applique $R', ÞR et "R' sans plus de ménagement, on obtient le séquent :

P (x', c) ¾® P (c, x')

que l'on peut clore en liant x' à c.

Pour empêcher cela, nous maintenons une base de données de dépendances. Chaque fois que nous créons une nouvelle constante c par les règles "R' ou $L', nous enregistrons les contraintes de dépendances c<y pour toute variable libre y dans le séquent courant : ceci formalise la condition de bord sur la variable universelle c, comme quoi c ne doit pas dépendre de y.

Il nous faut ensuite étendre le test d'occurrence de l'unification pour qu'il gère ces contraintes de dépendances supplémentaires : disons qu'un terme t dépend de x si et seulement si t=x, ou t est une constante c telle que la contrainte c<x soit dans la base de données, ou t=f(t₁,...,t_n) et un t_i, 1£ i£ n, dépend de x. Nous exigeons ensuite que les unificateurs les plus généraux soient trouvés comme des substitutions s telles que pour tout xÎdom s, xs ne dépend d'aucune variable de dom s.

d-règles

d d₁

+" x· F +F[c/x]

-$ x· F -F[c/x]
(où c est une nouvelle constante, et où nous ajoutons la contrainte c<y pour chaque variable libre y dans le chemin courant.)

Figure 3: d-règles en tableaux à variables libres

En jargon des tableaux, les règles "R' et $L' donnent lieu aux d-règles de la figure 3.

Nous pouvons désormais étendre la notion de chemins des tableaux à variables libres comme suit : si C est un chemin contenant une formule F de type g, alors CÈ {g₁} est aussi un chemin, où g₁ est défini comme dans la figure 2; et si C est un chemin contenant une formule F de type d, alors C\ {F}È {d₁} est encore un chemin, où d₁ est défini comme en figure 3. Une stratégie d'expansion équitable est alors une stratégie qui n'effectue pas une infinité d'étapes consécutives de g-expansions (autrement dit, d'étapes d'extension), et, comme en section 1, toute stratégie d'expansion équitable définit une procédure de recherche de preuve correcte et complète.

2.2 Herbrandisation au vol

On peut coder la base de données des dépendances des tableaux à variables libres de façon plus directe en produisant non pas des constantes c associées à des contraintes c<y₁, ...c<y_n, mais un terme unique f(y₁,...,y_n), où la dépendance est codée directement à l'intérieur du terme f(y₁,...,y_n). Ce n'est qu'une autre façon d'effectuer une herbrandisation, mais au vol.

L'ajout de nouvelles constantes ou de nouveaux symboles de fonction ne pose aucun problème en logique du premier ordre. Mais ce n'est pas le cas en logique d'ordre supérieur, parce que l'instantiation de variables d'ordres supérieurs peut propager l'introduction de constantes ou de variables dans d'autres formules. En fait, nous ne pouvons pas herbrandiser : dans ce cas, nous devons nous en tenir aux tableaux à variables libres, et même ne pas considérer c comme des constantes, mais comme des variables que l'on ne peut pas remplacer par d'autres termes [Koh95].

Il y a une autre raison pour laquelle nous souhaitons éviter de fabriquer de nouvelles constantes comme c, et c'est que cette méthode peut être très inefficace. La raison est que deux constantes c et c' créées à des instants différents lors du processus d'expansion ne s'unifient jamais. Ceci peut empêcher la procédure de tableaux d'arriver à clore des chemins rapidement, alors qu'il aurait été possible de le faire en instanciant la formule F de façon plus intelligente.

d⁺⁺-règles

d d₁

+" x· F +F[f(x₁,...,x_n)/x]

-$ x· F -F[f(x₁,...,x_n)/x]

(fv(F)\{x}={x₁,...,x_n}, f=l x₁· ..., l x_n· e x·F)

Figure 4: d⁺⁺-règles en tableaux à variables libres

Ce que les d-règles réalisent est juste l'herbrandisation ou la skolémisation; regardons donc la preuve du théorème de Herbrand-Skolem syntaxique plus en détail : pour expanser une formule de type d, disons +" x·F, nous devons remplacer x dans F par un terme t, tel que des instances différentes de " x·F doivent produire des instances différentes de t. Dans les règles ci-dessus, nous avons produit un nouveau terme t (sous la forme d'une constante nouvelle) à chaque fois que nous avons instancié F, de sorte que la condition est vérifiée. Mais nous pouvons faire mieux, et en particulier utiliser la d⁺⁺-règle de la figure 4, due à Peter Schmitt, Reiner Hähnle et Bernhard Beckert [BHS93]. Cette règle correspond aux règles de séquents suivantes :

où fv(F)\{x}={x₁,...,x_n}, et f est le symbole l x₁· ..., l x_n· e x·F, qui remplacent "R et $L. (e est traditionnellement appelé le symbole de choix de Hilbert.)

Pour construire le symbole de fonction de Skolem f, d'abord, nous renommons toutes les variables de F en des variables de noms canoniques; ensuite, nous fabriquons l'expression l x₁· ..., l x_n· e x·F, où x₁, ..., x_n sont les noms canoniques des variables, et F est supposée renommée. Une telle expression, où l est un opérateur lieur (comme " ou $), se représente sous forme arborescente comme les formules. Considérons maintenant cette expression, qui n'est ni un terme ni une formule de la logique du premier ordre, comme un nouveau symbole : il s'agit du symbole de Skolem souhaité.

Il peut sembler surprenant que nous décidions qu'une expression tout entière, et en fait même une l-expression, soit considérée comme un symbole, car nous sommes habitués à penser aux symboles comme à de simples chaînes de caractères; mais les symboles sont totalement arbitraires, et la seule contrainte sur les symboles est qu'il doit y en avoir une infinité.

On peut aussi se demander pourquoi nous produisons des symboles aussi compliqués d'apparence, alors qu'il suffisait de produire une constante nouvelle. Comme nous l'avons dit plus haut, fabriquer de nouvelles constantes peut augmenter de façon considérable la taille de la preuve à trouver. La d⁺⁺-règle est une des meilleures en termes de longueur de preuve. De plus, la production de nouveaux symboles de fonction de cette façon est très simple à réaliser, car nous avons déjà tout ce qu'il faut pour construire et comparer des formules.

Cette technique est important en particulier quand deux sous-formules quantifiées d'une formule à prouver sont identiques, ou quand elle contient des équivalences logiques. Par exemple, supposons que nous souhaitions prouver la formule :

Si nous expansons le tableau correspondant, nous obtenons :

où (6), (7), (8), (9) ont été obtenues par des règles a et b à partir de (1); (10), (11), (12), (13) ont été obtenues par des règles a et b à partir de (8), et (15), (16), (17), (18) ont été obtenues par des règles a et b à partir de (9). Remarquons que la quantification -$ x· Q(x) en (10) et en (15) est associée au même symbole de Herbrand-Skolem c en (14) et en(19) : ce tableau peut ensuite être clos par la substitution [c/x₁]. Mais si nous avions créé des constantes nouvelles pour herbrandiser (10) et (15), (14) serait de la forme -Q(c) et (19) serait de la forme -Q(c'), où c et c' seraient deux constantes distinctes, et nous ne pourrions pas clore le tableau sans réappliquer d'abord une étape d'extension (une g-règle) sur (2) pour obtenir suffisamment de variables pouvant être liées à toutes les constantes que nous avons créées.

Théorème 2 [Correction, complétude] Soit F une formule close. F est prouvable en LK si et seulement s'il existe une substitution s qui clôt une expansion du tableau initial +F.
Preuve : Soit LK⁺ le système de séquents formé par l'ajout des règles "R⁺, $L⁺, "L⁺ et $R⁺ à LK₀ sans coupure. L'expansion de tableau revient à développer des preuves en LK⁺ à partir du but (du bas vers le haut).

Nous devons donc montrer que nous pouvons transformer toute preuve p de LK sans coupure en un couple (p',s), où p' est une dérivation dans LK⁺ et s est une substitution qui instancie les séquents sans prémisses de p' en des instances de Ax. L'argument est par récurrence sur la profondeur de p. Les cas intéressants sont :

quand nous traduisons une dérivation se terminant en une application de $R (resp. "L) : alors nous avons dérivé G ¾® D, $ x·F de G ¾® D, F[t/x], qui est dérivé par une preuve strictement moins profonde. Affaiblissons ce dernier pour obtenir G ¾® D, $ x·F, F[t/x], que nous traduisons par hypothèse de récurrence en une dérivation dans LK⁺ de G ¾® D, $ x·F, F[t/x] et une substitution s'; il s'agit aussi d'une dérivation dans LK⁺ de G ¾® D, $ x·F, F[x'/x], où x' est une nouvelle variable, pour la substitution s'[t/x']; appliquons ensuite $R' pour en déduire la dérivation désirée dans LK⁺ et la substitution s=s'[t/x']. (Idem pour "L.)
quand nous traduisons une dérivation se terminant par une application de "R (resp. $L) : alors nous avons dérivé G ¾® D, " x·F de G ¾® D, F[x'/x], avec x' une nouvelle variable. Ce dernier séquent est dérivé par une preuve strictement moins profonde. Remplaçons x' dans toute la preuve par le terme de Herbrand-Skolem f(x₁,...,x_n), où x₁, ..., x_n sont les variables libres de F moins x, alors nous en obtenons une preuve de même profondeur de G ¾® D, F[f(x₁,...,x_n)/x], que nous traduisons par hypothèse de récurrence en une dérivation dans LK⁺ du même séquent, avec comme substitution s. Appliquons ensuite "R⁺ pour en déduire la dérivation désirée dans LK⁺ et la substitution s. (De même pour $L.)

Réciproquement, nous devons montrer que nous pouvons transformer tout couple (p',s), où p' est une dérivation dans LK⁺ et s instancie tous les séquents sans prémisses de p' en des instances de Ax, en une preuve de LK. Ceci se montre comme avant, sauf que dans les cas de "R et de $L, nous réutilisons les arguments de la preuve du théorème de Herbrand-Skolem syntaxique pour remplacer les termes de Herbrand-Skolem par des variables et réobtenir une preuve dans LK. ¤

On peut renforcer ce théorème en disant que, si une telle substitution s existe, alors nous pouvons en trouver une en cherchant un unificateur simultané de toutes les paires de formules complémentaires sur les chemins du tableaux expansé de +F, comme en section 1. Ceci termine notre justification des tableaux à variables libres.

2.3 Discussion

Le premier avantage qu'ont les tableaux à variables libres sur les tableaux de la section 1 est qu'il n'est plus nécessaire d'effectuer un quelconque pré-traitement sur la formule que nous souhaitons prouver. Ce n'est pas tellement un avantage en logique classique, car nous referons le travail d'herbrandisation et de skolémisation pendant la preuve plutôt qu'avant. Mais c'est crucial si l'on désire adapter la méthode aux logiques non classiques comme la logique intuitionniste. Observons en particulier que les tableaux à variables libres opèrent essentiellement de la même façon en logique intuitionniste : nous devons juste vérifier qu'aucun chemin n'a jamais plus d'une formule positive. Rappelons aussi que la conversion en forme prénexe ou la skolémisation à l'avance ne préservent pas la prouvabilité en logique intuitionniste, de sorte que les tableaux à variables libres sont essentiellement la seule méthode raisonnable. L'argument serait tout aussi vrai pour les logiques linéaire, de la pertinence (``relevant logic'') ou les logiques modales.

Le deuxième avantage des tableaux à variables libres est que la recherche d'une preuve est confinée à une recherche de preuves sans coupures, ce qui forme un espace beaucoup plus étroit que l'espace des preuves générales. Ce n'est pas encore aussi réduit que l'espace exploré par les raffinements les plus efficaces de la résolution en logique classique, mais nous verrons en section 3.4 qu'il n'est pas besoin de beaucoup contraindre les tableaux pour obtenir un des raffinements les plus puissants de la résolution, l'élimination de modèles.

Le troisième avantage des tableaux à variables libres, qu'ils ont en commun avec la première méthode de tableaux que nous avons présentée dans ce chapitre, est que même si nous insistons pour skolémiser à l'avance, il n'est pas nécessaire de convertir la formule à prouver en forme clausale. C'est un avantage sur la résolution, car le calcul d'une forme clausale peut prendre un temps exponentiel en la taille de la formule d'entrée --- bien que ça n'arrive que rarement en pratique.

Les tableaux ont cependant de graves inconvénients. Ils essaient de trouver des preuves sans coupure en développant des preuves de LK ou de systèmes proches de LK sous forme d'arbres, et aucun partage entre les chemins n'est exploité, à part dans les préfixes de ces chemins. En particulier, une grande partie du travail doit être réeffectuée d'un chemin à l'autre. Ceci est un défaut que les raffinements de la résolution n'ont pas en général, parce que toutes les tentatives de trouver une réfutation sont enregistrées dans un ensemble unique de clauses, et restent donc toujours disponibles pour savoir ce qu'on peut éviter de refaire (typiquement, par le test de subsomption). Pour optimiser les tableaux de cette façon, il nous faudrait conserver des informations sur ce qui a été fait et ce qui a échoué d'un chemin sur l'autre. Le seul point positif dû à cette absence de partage entre les calculs effectués sur différents chemins est que cela facilite la parallélisation de la méthode de tableaux. Cependant, la parallélisation ne suffit pas pour faire des tableaux une méthode plus efficace que des algorithmes séquentiels, et les réalisations parallèles les plus élaborées des tableaux utilisent déjà des techniques supplémentaires pour éviter les redondances entre les chemins.

Un autre défaut des tableaux est que, bien que nous faisions appel à l'unification pour guider la recherche d'une preuve, il est possible que nous ayons à expanser les chemins complètement ou presque complètement avant d'atteindre le point où nous pouvons enfin unifier des formules atomiques. Au moment où nous avons suffisamment expansé les chemins pour calculer des unificateurs non triviaux, il peut nous rester sur les bras un nombre trop grand de chemins pour qu'on puisse tous les clore en temps raisonnable. Il peut en effet y en avoir un nombre exponentiel en la longueur du chemin.

Un dernier défaut des tableaux est qu'il reste une certaine redondance dans l'espace de toutes les preuves sans coupure, due aux permutabilités. En logique classique, ce n'est pas grave : la plupart des règles permutent, et donc nous pouvons utiliser n'importe quelle stratégie d'expansion, au moins pour ce qui est des connecteurs propositionnels. Les seules impermutabilités proviennent des règles sur les quantificateurs, et nous les avons codées par des termes de Skolem (ou des contraintes de dépendances) : l'essence du théorème 2 est en effet que nous avons remplacé LK, un système avec trois impermutabilités, par LK⁺, un système sans impermutabilités mais avec une condition d'unifiabilité plus complexe. Cette idée de coder les impermutabilitées sous forme de termes de Skolem s'étend aux systèmes de séquents pour les logiques non classiques [Sha92].

d⁺⁺-règles
d	d₁
+" x· F	+F[f(x₁,...,x_n)/x]
-$ x· F	-F[f(x₁,...,x_n)/x]