Un conjunto de estructuras de datos y técnicas algorítmicas para organizar términos, subtérminos o cláusulas de modo que coincidencias sintácticas, socios de unificación u ocurrencias de patrones se puedan recuperar rápidamente durante el razonamiento automatizado.

Principio

Aprovechar características discriminantes compactas de los términos (símbolos, rutas, huellas, posiciones) para evitar comparaciones exhaustivas; las estructuras de índice intercambian coste de espacio y de actualización por una búsqueda de candidatos rápida en tiempo de consulta, manteniendo la corrección para el matching sintáctico o la unificación.

Demostración

En un demostrador por saturación, un árbol de discriminación indexa términos por su secuencia de símbolos de modo que, al seleccionar un literal f(a, X) para resolver, se recuperan solo las cláusulas que contienen términos unificables con cabeza f en vez de escanear toda la base de cláusulas. Otro ejemplo es un árbol de sustituciones que enumera todos los términos que unifican con una consulta y devuelve identificadores de cláusulas en tiempo sublineal respecto al tamaño de la base.

Aplicación incorrecta

Usar un índice basado únicamente en el símbolo raíz para consultas que requieren coincidencia estructural de sub-términos produce muchos candidatos falsos y ningún ahorro temporal; igualmente, crear índices extremadamente especializados sin considerar el coste de actualización puede hacer que la adición incremental de lemas sea prohibitivamente cara en demostradores interactivos.

Consecuencia

Los índices de términos bien diseñados reducen el número de intentos de unificación sintáctica costosos, disminuyen drásticamente los tiempos de los demostradores y la fragmentación de memoria en grandes bases de conocimiento, y permiten servicios escalables como la selección de premisas y la simplificación basada en matching.

Inversión

Sin indexación de términos, el sistema debe realizar comparaciones exhaustivas término a término o búsquedas por barrido completo; el contraste invertido es un índice orientado a consultas semánticas basadas en modelos (p. ej., indexación de valoraciones) que persigue objetivos de recuperación distintos y puede no servir para la unificación sintáctica.

Límite

Se aplica a problemas de recuperación sintáctica (coincidencias exactas, coincidencias de patrones, unificación sintáctica). No proporciona por sí mismo consecuencia semántica, comprobación de modelos ni búsqueda de similitud probabilística; excluye técnicas de incrustación puramente estadísticas, salvo si se usan explícitamente como capas aproximadas de índice.

Tensión semántica

Existe tensión entre índices compactos y rápidos de actualizar que devuelven muchos candidatos amplios (alto recall, baja precisión) y índices estructurales ricos que son precisos pero costosos de mantener; otra tensión es la optimización para construcción por lotes frente al uso incremental interactivo.

Síntesis

La indexación de términos consiste en elegir y organizar características estructurales discriminantes de términos en estructuras de datos (árboles de discriminación, árboles de sustitución, hashes de firmas, índices de rutas) para que los razonadores automáticos reduzcan rápidamente conjuntos de candidatos para matching y unificación, equilibrando velocidad de recuperación con costes de espacio y actualización.