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 de teoremas automatizado .

Descripción general

Muchas operaciones en demostradores automáticos de teoremas requieren búsquedas en enormes colecciones de términos y cláusulas. Estas operaciones suelen encajar en el siguiente esquema. Dada una colección de términos (cláusulas) y un término de consulta (cláusula) , busque en algunos/todos los términos relacionados de acuerdo con 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 relacione de manera especial la consulta y los objetos recuperados . A continuación se muestra una lista de condiciones de recuperación que se utilizan con frecuencia en los probadores: ${\displaystyle S}$ ${\displaystyle q}$ ${\displaystyle S}$ ${\displaystyle t}$ ${\displaystyle q}$ ${\displaystyle t}$

• término es unificable con término , es decir, existe una sustitución , tal que = ${\displaystyle q}$ ${\displaystyle t}$ ${\displaystyle \theta }$ ${\displaystyle q\theta }$ ${\displaystyle t\theta }$
• término es una instancia de , es decir, existe una sustitución tal que = ${\displaystyle t}$ ${\displaystyle q}$ ${\displaystyle \theta }$ ${\displaystyle q\theta }$ ${\displaystyle t}$
• El término es una generalización de , es decir, existe una sustitución tal que = ${\displaystyle t}$ ${\displaystyle q}$ ${\displaystyle \theta }$ ${\displaystyle q}$ ${\displaystyle t\theta }$
• cláusula θ-subsume la cláusula , es decir, existe una sustitución , tal que es un subconjunto/submulticonjunto de ${\displaystyle q}$ ${\displaystyle t}$ ${\displaystyle \theta }$ ${\displaystyle q\theta }$ ${\displaystyle t}$
• cláusula está θ-subsumida por , es decir, existe una sustitución , tal que es un subconjunto/submulticonjunto de ${\displaystyle q}$ ${\displaystyle t}$ ${\displaystyle \theta }$ ${\displaystyle t\theta }$ ${\displaystyle q}$

La mayoría de las veces, estamos interesados ​​en encontrar explícitamente las sustituciones apropiadas, junto con los términos recuperados , en lugar de simplemente establecer la existencia de tales sustituciones. ${\displaystyle t}$

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

Técnicas de indexación clásicas

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

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]

Técnicas de indexación utilizadas en la programación lógica.

La indexación del primer argumento es la estrategia más común en la que el primer argumento se utiliza como índice. Distingue valores atómicos y el funtor principal de términos compuestos.

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

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

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

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

Referencias

1. Colomb, Robert M. (1991). "Mejora de la unificación en PROLOG mediante indexación de cláusulas". La revista de programación lógica . 10 : 23–44. doi :10.1016/0743-1066(91)90004-9.
2. Peter Graf. "Indexación de árbol de sustitución". 1994.
3. John W. Wheeler; Guarionex Jordania. "Un estudio empírico de la indexación de términos en la implementación de Darwin del cálculo de la evolución del modelo". 2004. pág. 5.
4. Körner, Philipp; Leuschel, Michael; Barbosa, João; Costa, Vítor Santos; Dahl, Verónica; Hermenegildo, Manuel V.; Morales, José F.; Wielemaker, enero; Díaz, Daniel; Abreu, Salvador; Ciatto, Giovanni (2022). "Cincuenta años de prólogo y más allá". Teoría y práctica de la programación lógica . 22 (6): 776–858. doi :10.1017/S1471068422000102. hdl : 10174/33387 . ISSN  1471-0684. Este artículo incorpora texto de esta fuente, que está disponible bajo la licencia CC BY 4.0.

Otras lecturas

• P. Graf, Term Indexing, Lecture Notes in Computer Science 1053, 1996 (descripción general ligeramente desactualizada)
• R. Sekar y IV Ramakrishnan y A. Voronkov, Term Indexing, en A. Robinson y A. Voronkov, editores, Handbook of Automated Reasoning , volumen 2, 2001 (resumen 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, Proc. de RTA, Apuntes de conferencias sobre informática 914, 1995
• M. Stickel, El método de indexación de rutas para términos de indexación, Tech. Rep. 473, Centro de Inteligencia Artificial , SRI Internacional , 1989
• S. Schulz, Subsunción de cláusulas simple y eficiente con indexación de vectores de características, Proc. del taller IJCAR-2004 ESFOR, 2004
• A. Riazanov y A. Voronkov, Árboles de código parcialmente adaptativos, Proc. JELIA, Apuntes de conferencias sobre inteligencia artificial 1919, 2000
• H. Ganzinger y 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, información y computación de rutas estándar y relacionales, 199 (1–2), 2005