| dbpprop:abstract
|
- In computer science, term indexing is the task of creating an index of terms and clauses in a collection. Many operations in automatic theorem provers require search in huge collections of terms and clauses. Such operations typically fall into the following scheme. Given a collection <math>S</math> of terms (clauses) and a query term (clause) <math>q</math>, find in <math>S</math> some/all terms <math>t</math> related to <math>q</math> according to a certain retrieval condition. Most interesting retrieval conditions are formulated as existence of a substitution that relates in a special way the query and the retrieved objects <math>t</math>. Here is a list of retrieval conditions frequently used in provers: term <math>q</math> is unifiable with term <math>t</math>, i.e. , there exists a substitution <math> \theta </math>, such that <math>q\theta</math> = <math>t\theta</math> term <math>t</math> is an instance of <math>q</math>, i.e. , there exists a substitution <math>\theta</math>, such that <math>q\theta</math> = <math>t</math> term <math>t</math> is a generalisation of <math>q</math>, i.e. , there exists a substitution <math>\theta</math>, such that <math>q</math> = <math>t\theta</math> clause <math>q</math> subsumes clause <math>t</math>, i.e. , there exists a substitution <math>\theta</math>, such that <math>q\theta</math> is a subset/submultiset of <math>t</math> clause <math>q</math> is subsumed by <math>t</math>, i.e. , there exists a substitution <math>\theta</math>, such that <math>t\theta</math> is a subset/submultiset of <math>q</math> More often than not, we are actually interested in finding the appropriate substitutions explicitly, together with the retrieved terms <math>t</math>, rather than just in establishing existence of such substitutions. Very often the sizes of term sets to be searched are large, the retrieval calls are frequent and the retrieval condition test is rather complex. In such situations linear search in <math>S</math>, when the retrieval condition is tested on every term from <math>S</math>, becomes prohibitively costly. To overcome this problem, special data structures, called indexes, are designed in order to support fast retrieval. Such data structures, together with the accompanying algorithms for index maintenance and retrieval, are called term indexing techniques.
- L’index terminologique est utilisé pour lister les termes significatifs utilisés dans un ouvrage, avec renvoi aux pages auxquelles ils sont utilisés. Par extension, en informatique, l'indexation de termes est la tâche qui consiste à créer un index de termes et les clauses de la collecte.
- Indeksowanie termów to zagadnienie polegające na wyszukaniu w pewnym zbiorze termów tych termów (dowolnego albo też wszystkich), które są w pewnej relacji z danym termem. Zagadnieniem temu w szczególności poświęcony jest dział z pogranicza informatyki i matematyki zwany: Systemy Wyszukiwania Informacji. Indeksowanie termów ma wiele zastosowań, ale w większości typowych problemów termów jest mało i są proste, a ich zbiór jest stały. Zupełnie inaczej ma się to w przypadku systemów automatycznego dowodzenia twierdzeń - tam termów jest dużo, są złożone, i cały czas następuje ich dodawanie i kasowanie. Dobre algorytmy indeksowania termów są więc kluczowe dla wydajności takich systemów. Ważniejsze algorytmy indeksowania termów to: code tree context tree drzewo dyskryminacyjne (teoria obliczeń) substitution tree
|
| rdfs:comment
|
- In computer science, term indexing is the task of creating an index of terms and clauses in a collection. Many operations in automatic theorem provers require search in huge collections of terms and clauses. Such operations typically fall into the following scheme.
- L’index terminologique est utilisé pour lister les termes significatifs utilisés dans un ouvrage, avec renvoi aux pages auxquelles ils sont utilisés. Par extension, en informatique, l'indexation de termes est la tâche qui consiste à créer un index de termes et les clauses de la collecte.
- Indeksowanie termów to zagadnienie polegające na wyszukaniu w pewnym zbiorze termów tych termów (dowolnego albo też wszystkich), które są w pewnej relacji z danym termem. Zagadnieniem temu w szczególności poświęcony jest dział z pogranicza informatyki i matematyki zwany: Systemy Wyszukiwania Informacji. Indeksowanie termów ma wiele zastosowań, ale w większości typowych problemów termów jest mało i są proste, a ich zbiór jest stały.
|
![[RDF Data]](/statics/sw-cube.png)
