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 .
Descripción general
Muchas operaciones en los probadores automáticos de teoremas requieren una búsqueda en grandes colecciones de términos y cláusulas. Estas operaciones suelen caer en el siguiente esquema. Dada una colección de términos (cláusulas) y un término de consulta (cláusula) , Encontrar en algunos / todos los términos relacionado con 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.. Aquí hay una lista de condiciones de recuperación que se utilizan con frecuencia en los probadores:
- término es unificable con el término , es decir, existe una sustitución , tal que =
- término es una instancia de , es decir, existe una sustitución , tal que =
- término es una generalización de , es decir, existe una sustitución , tal que =
- cláusula cláusula subsume , es decir, existe una sustitución , tal que es un subconjunto / submultiset de
- cláusula está subsumido por , es decir, existe una sustitución , tal que es un subconjunto / submultiset de
La mayoría de las veces, estamos realmente interesados en encontrar explícitamente las sustituciones apropiadas, junto con los términos recuperados. , en lugar de simplemente establecer la existencia de tales sustituciones.
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 condición 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 costoso. Para superar este problema, se diseñan estructuras de datos especiales, denominadas índices , con el fin de admitir 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 .
Técnicas clásicas de indexación
- árboles de discriminación
- árboles de sustitución
- indexación de ruta
Los árboles de sustitución superan 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 de prueba . [3]
Técnicas modernas de indexación
- indexación de vectores de características
- árboles de código
- árboles de contexto
- indexación de ruta relacional
Referencias
- ^ Colomb, Robert M. (1991). "Mejora de la unificación en PROLOG mediante la indexación de cláusulas". El diario de la programación lógica . 10 : 23–44. doi : 10.1016 / 0743-1066 (91) 90004-9 .
- ^ Peter Graf. "Indexación del árbol de sustitución" . 1994.
- ^ John W. Wheeler; Guarionex Jordan. "Un estudio empírico de la indexación de términos en la implementación de Darwin del modelo de cálculo de evolución" . 2004. p. 5.
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 la indexación de árboles de discriminación y la indexación de rutas para la recuperación de términos, Journal of Automated Reasoning, 9 (2), 1992
- P. Graf, Indización de árboles de sustitución, Proc. of RTA, Lecture Notes in Computer Science 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 International , 1989
- S. Schulz, Subsunción de cláusulas simples y eficientes 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 adaptables, Proc. JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
- H. Ganzinger y R. Nieuwenhuis y P. Nivela, Indexación de término rápido con árboles de contexto codificados, Journal of Automated Reasoning, 32 (2), 2004
- A. Riazanov y A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199 (1–2), 2005