Une famille de structures de données et d'algorithmes destinés à organiser des termes, sous-terms ou clauses afin de retrouver rapidement des correspondances syntaxiques, des partenaires d'unification ou des occurrences de motifs lors du raisonnement automatisé.

Principe

Exploiter des caractéristiques discriminantes compactes des termes (symboles, chemins, empreintes, positions) pour éviter les comparaisons exhaustives ; les structures d'index font le compromis entre espace et coût de mise à jour et une récupération rapide des candidats à la requête tout en garantissant la correction pour les correspondances syntaxiques ou l'unification.

Démonstration

Dans un démonstrateur par saturation, un arbre de discrimination indexe les termes selon la séquence de symboles de sorte que, lors de la sélection d'un littéral f(a, X) pour la résolution, on récupère seulement les clauses contenant des termes unifiables avec tête f au lieu de scanner toute la base de clauses. Un autre exemple est l'arbre de substitutions qui énumère les termes unifiables avec une requête et renvoie les identifiants de clauses en temps sous-linéaire par rapport à la taille de la base.

Mauvaise application

Utiliser un index fondé uniquement sur le symbole racine pour des requêtes qui exigent une correspondance structurelle de sous-termes entraîne de nombreux faux candidats et aucun gain de temps ; à l'inverse, créer des index excessivement spécialisés sans tenir compte du coût de mise à jour peut rendre l'ajout incrémental de lemmes prohibitif dans des prouveurs interactifs.

Conséquence

Des index de termes bien conçus réduisent le nombre d'essais d'unification syntaxiques coûteux, diminuent fortement les temps d'exécution du prouveur et l'érosion mémoire sur de larges bases de connaissances, et permettent des services évolutifs comme la sélection d'axiomes et la simplification par appariement.

Inversion

Sans indexation de termes, le système doit effectuer des comparaisons exhaustives terme-à-terme ou des recherches par balayage complet ; le contraste inverse est un index conçu pour des requêtes sémantiques orientées modèle (p. ex. indexation de valuations) qui vise d'autres objectifs de récupération et peut ne pas convenir à l'unification syntaxique.

Limite

S'applique aux problèmes de récupération syntaxique (correspondances exactes, correspondances de motifs, unification syntaxique). Ne fournit pas en soi d'implication sémantique, de vérification de modèles ni de recherche de similarité probabiliste ; exclut les techniques d'incorporation purement statistiques sauf si elles sont explicitement utilisées comme couches d'index approximatives.

Tension sémantique

Il existe une tension entre des index compacts et rapides à mettre à jour qui rendent de nombreux candidats grossiers (forte rappel, faible précision) et des index structurels riches qui sont précis mais coûteux à maintenir ; une autre tension oppose l'optimisation pour construction par lot à l'utilisation incrémentale interactive.

Synthèse

L'indexation de termes consiste à choisir et organiser des caractéristiques structurelles discriminantes des termes dans des structures de données (arbres de discrimination, arbres de substitutions, hachages de signatures, index de chemins) afin que les moteurs de raisonnement automatisés réduisent rapidement les ensembles de candidats pour l'appariement et l'unification, en équilibrant vitesse de récupération, espace et coûts de mise à jour.