Indexação de termos - Term indexing

Na ciência da computação , um índice de termos é uma estrutura de dados para facilitar a pesquisa rápida de termos e cláusulas em um programa lógico , banco de dados dedutivo ou provador automatizado de teoremas .

Visão geral

Muitas operações em provadores automáticos de teoremas requerem pesquisa em enormes coleções de termos e cláusulas. Essas operações normalmente se enquadram no seguinte esquema. Dada uma coleção de termos (cláusulas) e um termo de consulta (cláusula) , encontre em alguns / todos os termos relacionados de acordo com uma determinada condição de recuperação. As condições de recuperação mais interessantes são formuladas como a existência de uma substituição que relaciona de maneira especial a consulta e os objetos recuperados . Aqui está uma lista de condições de recuperação frequentemente usadas em provadores: ${\ displaystyle S}$${\ displaystyle q}$${\ displaystyle S}$${\ displaystyle t}$${\ displaystyle q}$${\ displaystyle t}$

• termo é unificável com termo , ou seja, existe uma substituição , tal que =${\ displaystyle q}$${\ displaystyle t}$${\ displaystyle \ theta}$${\ displaystyle q \ theta}$${\ displaystyle t \ theta}$
• termo é uma instância de , ou seja, existe uma substituição , tal que =${\ displaystyle t}$${\ displaystyle q}$${\ displaystyle \ theta}$${\ displaystyle q \ theta}$${\ displaystyle t}$
• termo é uma generalização de , ou seja, existe uma substituição , tal que =${\ displaystyle t}$${\ displaystyle q}$${\ displaystyle \ theta}$${\ displaystyle q}$${\ displaystyle t \ theta}$
• cláusula cláusula subsume cláusula , ou seja, existe uma substituição , tal que é um subconjunto / submultiset de${\ displaystyle q}$${\ displaystyle t}$${\ displaystyle \ theta}$${\ displaystyle q \ theta}$${\ displaystyle t}$
• cláusula é subsumida por , ou seja, existe uma substituição , tal que é um subconjunto / submultiset de${\ displaystyle q}$${\ displaystyle t}$${\ displaystyle \ theta}$${\ displaystyle t \ theta}$${\ displaystyle q}$

Na maioria das vezes, estamos realmente interessados ​​em encontrar as substituições apropriadas explicitamente, junto com os termos recuperados , ao invés de apenas estabelecer a existência de tais substituições. ${\ displaystyle t}$

Muitas vezes, os tamanhos dos conjuntos de termos a serem pesquisados ​​são grandes, as chamadas de recuperação são frequentes e o teste de condição de recuperação é bastante complexo. Em tais situações, a pesquisa linear em , quando a condição de recuperação é testada em todos os termos de , torna-se proibitivamente cara. Para superar esse problema, estruturas de dados especiais, chamadas de índices , são projetadas para oferecer suporte à recuperação rápida. Essas estruturas de dados, junto com os algoritmos de acompanhamento para manutenção e recuperação de índices, são chamadas de técnicas de indexação de termos . ${\ displaystyle S}$${\ displaystyle S}$

Técnicas clássicas de indexação

• árvores de discriminação
• árvores de substituição
• indexação de caminho

As árvores de substituição superam a indexação de caminho, a indexação da árvore de discriminação e as árvores de abstração.

Um índice de termos de árvore de discriminação armazena suas informações em uma estrutura de dados trie .

Técnicas de indexação modernas

• indexação de vetor de recursos
• árvores de código
• árvores de contexto
• indexação de caminho relacional

Referências

Leitura adicional

• P. Graf, indexação de termos, notas de aula em ciência da computação 1053, 1996 (visão geral ligeiramente desatualizada)
• R. Sekar e IV Ramakrishnan e A. Voronkov, Indexação de termos, em A. Robinson e A. Voronkov, editores, Handbook of Automated Reasoning , volume 2, 2001 (visão geral recente)
• WW McCune, Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval, Journal of Automated Reasoning, 9 (2), 1992
• P. Graf, Substitution Tree Indexing, Proc. of RTA, Lecture Notes in Computer Science 914, 1995
• M. Stickel, The Path Indexing Method for Indexing Terms, Tech. Rep. 473, Artificial Intelligence Center , SRI International , 1989
• S. Schulz, Simple and Efficient Clause Subsumption with Feature Vector Indexing, Proc. do workshop IJCAR-2004 ESFOR, 2004
• A. Riazanov e A. Voronkov, Partially Adaptive Code Trees, Proc. JELIA, Notas de aula em Inteligência Artificial 1919, 2000
• H. Ganzinger e R. Nieuwenhuis e P. Nivela, Fast Term Indexing with Coded Context Trees, Journal of Automated Reasoning, 32 (2), 2004
• A. Riazanov e A. Voronkov, Efficient Instance Retrieval with Standard and Relational Path Indexing, Information and Computation, 199 (1-2), 2005