Indexación de términos

En informática , un índice de términos es una estructura de datos para facilitar la búsqueda rápida de términos y cláusulas en un programa lógico , ^{[ 1 ]} base de datos deductiva o demostrador automático de teoremas .

Muchas operaciones en los demostradores automáticos de teoremas requieren búsqueda en enormes colecciones de términos y cláusulas. Dichas operaciones suelen seguir el siguiente esquema. Dada una colección${\displaystyle S}$de términos (cláusulas) y un término de consulta (cláusula)${\displaystyle q}$, encontrar en${\displaystyle S}$algunos/todos los términos${\displaystyle t}$relacionado con${\displaystyle q}$según una determinada condición de recuperación. Las condiciones de recuperación más interesantes se formulan como la existencia de una sustitución que relaciona de manera especial la consulta y los objetos recuperados.${\displaystyle t}$Aquí hay una lista de condiciones de recuperación que se utilizan con frecuencia en los demostradores:

• término${\displaystyle q}$es unificable con término${\displaystyle t}$, es decir, existe una sustitución${\displaystyle \theta }$, de tal manera que${\displaystyle q\theta }$=${\displaystyle t\theta }$
• término${\displaystyle t}$es un ejemplo de${\displaystyle q}$, es decir, existe una sustitución${\displaystyle \theta }$, de tal manera que${\displaystyle q\theta }$=${\displaystyle t}$
• término${\displaystyle t}$es una generalización de${\displaystyle q}$, es decir, existe una sustitución${\displaystyle \theta }$, de tal manera que${\displaystyle q}$=${\displaystyle t\theta }$
• cláusula${\displaystyle q}$cláusula θ-subsumes${\displaystyle t}$, es decir, existe una sustitución${\displaystyle \theta }$, de tal manera que${\displaystyle q\theta }$es un subconjunto/submulticonjunto de${\displaystyle t}$
• cláusula${\displaystyle q}$es θ-subsumido por${\displaystyle t}$, es decir, existe una sustitución${\displaystyle \theta }$, de tal manera que${\displaystyle t\theta }$es un subconjunto/submulticonjunto de${\displaystyle q}$

En la mayoría de los casos, lo que realmente nos interesa es encontrar explícitamente las sustituciones adecuadas, junto con los términos recuperados.${\displaystyle t}$, en lugar de limitarse a establecer la existencia de tales sustituciones.

Muy a menudo, los tamaños de los conjuntos de términos a buscar son grandes, las llamadas de recuperación son frecuentes y la prueba de condición de recuperación es bastante compleja. En tales situaciones, la búsqueda lineal en${\displaystyle S}$, cuando la condición de recuperación se prueba en cada término de${\displaystyle S}$Esto se vuelve prohibitivamente costoso. Para superar este problema, se diseñan estructuras de datos especiales, llamadas índices , para facilitar la recuperación rápida. Estas estructuras de datos, junto con los algoritmos correspondientes para el mantenimiento y la recuperación de índices, se denominan técnicas de indexación de términos .

• árboles de discriminación
• árboles de sustitución
• indexación de rutas

Los árboles de sustitución superan a la indexación de rutas, la indexación de árboles de discriminación y los árboles de abstracción. ^{[ 2 ]}

Un índice de términos de árbol de discriminación almacena su información en una estructura de datos trie . ^{[ 3 ]}

La indexación por primer argumento es la estrategia más común, donde el primer argumento se utiliza como índice. Permite distinguir los valores atómicos y el functor principal de los términos compuestos.

La indexación de argumentos distintos al primero es una variante de la indexación de argumentos que utiliza técnicas iguales o similares a las de la indexación de argumentos en uno o más argumentos alternativos. Por ejemplo, si una llamada a un predicado utiliza variables para el primer argumento, el sistema puede optar por usar el segundo argumento como índice.

La indexación de múltiples argumentos crea un índice combinado sobre varios argumentos instanciados si no existe un índice de un solo argumento suficientemente selectivo.

La indexación profunda se utiliza cuando varias cláusulas emplean el mismo functor principal para algún argumento. Aplica recursivamente técnicas de indexación iguales o similares a los argumentos de los términos compuestos.

La indexación Trie utiliza un árbol de prefijos para encontrar cláusulas aplicables. ^{[ 4 ]}

• P. Graf, Indexación de términos, Lecture Notes in Computer Science 1053, 1996 (descripción general ligeramente desactualizada)
• R. Sekar, IV Ramakrishnan y A. Voronkov, Indexación de términos, en A. Robinson y A. Voronkov, editores, Manual de razonamiento automatizado , volumen 2, 2001 (visión general reciente)
• WW McCune, Experimentos con indexación de árboles de discriminación e indexación de rutas para la recuperación de términos, Journal of Automated Reasoning, 9(2), 1992
• P. Graf, Indexación de árboles de sustitución, Actas de RTA, Lecture Notes in Computer Science 914, 1995
• M. Stickel, Método de indexación de rutas para la indexación de términos, Informe técnico 473, Centro de Inteligencia Artificial , SRI International , 1989.
• S. Schulz, Subsunción de cláusulas simple y eficiente con indexación de vectores de características, Actas del taller ESFOR de IJCAR-2004, 2004
• A. Riazanov y A. Voronkov, Árboles de código parcialmente adaptativos, Actas de JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
• H. Ganzinger, R. Nieuwenhuis y P. Nivela, Indexación rápida de términos con árboles de contexto codificados, Journal of Automated Reasoning, 32(2), 2004
• A. Riazanov y A. Voronkov, Recuperación eficiente de instancias con indexación de rutas estándar y relacionales, Information and Computation, 199(1–2), 2005