Индексация терминов

В информатике индекс терминов — это структура данных, облегчающая быстрый поиск терминов и предложений в логической программе , [1] дедуктивной базе данных или автоматизированной программе доказательства теорем .

Обзор

Многие операции в автоматических доказывателях теорем требуют поиска в огромных коллекциях терминов и предложений. Такие операции обычно укладываются в следующую схему. Дана коллекция терминов (предложений) и запросный термин (предложение) , найти некоторые/все термины, связанные с в соответствии с определенным условием поиска. Наиболее интересные условия поиска формулируются как существование подстановки, которая особым образом связывает запрос и извлеченные объекты . Вот список условий поиска, часто используемых в доказывателях: С {\displaystyle S} д {\displaystyle д} С {\displaystyle S} т {\displaystyle т} д {\displaystyle д} т {\displaystyle т}

  • термин унифицируем с термином , т.е. существует подстановка , такая что = д {\displaystyle д} т {\displaystyle т} θ {\displaystyle \тета} д θ {\displaystyle q\тета } т θ {\displaystyle t\тета }
  • term является экземпляром , т.е. существует подстановка , такая что = т {\displaystyle т} д {\displaystyle д} θ {\displaystyle \тета} д θ {\displaystyle q\тета } т {\displaystyle т}
  • Термин является обобщением , т.е. существует подстановка , такая что = т {\displaystyle т} д {\displaystyle д} θ {\displaystyle \тета} д {\displaystyle д} т θ {\displaystyle t\тета }
  • предложение θ-подключает предложение , т.е. существует подстановка , такая, что является подмножеством/подмультимножеством д {\displaystyle д} т {\displaystyle т} θ {\displaystyle \тета} д θ {\displaystyle q\тета } т {\displaystyle т}
  • предложение θ-включается в , т.е. существует подстановка , такая что является подмножеством/подмультимножеством д {\displaystyle д} т {\displaystyle т} θ {\displaystyle \тета} т θ {\displaystyle t\тета } д {\displaystyle д}

Чаще всего мы на самом деле заинтересованы в явном нахождении соответствующих замен вместе с извлеченными терминами , а не просто в установлении существования таких замен. т {\displaystyle т}

Очень часто размеры наборов терминов, в которых осуществляется поиск, велики, вызовы поиска часты, а проверка условий поиска довольно сложна. В таких ситуациях линейный поиск в , когда условие поиска проверяется для каждого термина из , становится непозволительно затратным. Чтобы преодолеть эту проблему, разрабатываются специальные структуры данных, называемые индексами , для поддержки быстрого поиска. Такие структуры данных вместе с сопутствующими алгоритмами для обслуживания индекса и поиска называются методами индексации терминов . С {\displaystyle S} С {\displaystyle S}

Классические методы индексации

  • деревья дискриминации
  • деревья замещения
  • индексация пути

Деревья подстановки превосходят индексацию путей, индексацию деревьев дискриминации и деревья абстракции. [2]

Индекс термина дерева дискриминации хранит свою информацию в структуре данных trie . [3]

Методы индексации, используемые в логическом программировании

Индексация первого аргумента — наиболее распространенная стратегия, где первый аргумент используется как индекс. Она различает атомарные значения и главный функтор составных терминов.

Индексация непервого аргумента — это разновидность индексации первого аргумента, которая использует те же или похожие методы, что и индексация первого аргумента для одного или нескольких альтернативных аргументов. Например, если вызов предиката использует переменные для первого аргумента, система может выбрать использование второго аргумента в качестве индекса.

Многоаргументное индексирование создает объединенный индекс по нескольким инстанцированным аргументам, если нет достаточно селективного индекса с одним аргументом.

Глубокая индексация используется, когда несколько предложений используют один и тот же главный функтор для некоторого аргумента. Она рекурсивно использует те же или похожие методы индексации для аргументов составных терминов.

Индексация Trie использует дерево префиксов для поиска применимых предложений. [4]

Ссылки

  1. ^ Коломб, Роберт М. (1991). «Улучшение унификации в PROLOG посредством индексации предложений». Журнал логического программирования . 10 : 23– 44. doi :10.1016/0743-1066(91)90004-9.
  2. ^ Питер Граф. «Индексирование дерева подстановок». 1994.
  3. ^ Джон В. Уилер; Гуарионекс Джордан. «Эмпирическое исследование индексации терминов в дарвиновской реализации эволюционного исчисления моделей». 2004. стр. 5.
  4. ^ Кернер, Филипп; Леушель, Майкл; Барбоза, Жуан; Коста, Витор Сантос; Даль, Вероника; Эрменегильдо, Мануэль В.; Моралес, Хосе Ф.; Вилемакер, Ян; Диас, Дэниел; Абреу, Сальвадор; Чатто, Джованни (2022). «Пятьдесят лет Пролога и не только». Теория и практика логического программирования . 22 (6): 776–858 . doi : 10.1017/S1471068422000102. hdl : 10174/33387 . ISSN  1471-0684. В данной статье использован текст из этого источника, доступный по лицензии CC BY 4.0.

Дальнейшее чтение

  • P. Graf, Term Indexing, Lecture Notes in Computer Science 1053, 1996 (немного устаревший обзор)
  • Р. Секар, И. В. Рамакришнан и А. Воронков, Индексирование терминов, в книге А. Робинсона и А. Воронкова, редакторов, Справочник по автоматизированному рассуждению , том 2, 2001 (последний обзор)
  • WW McCune, Эксперименты с индексацией дерева дискриминации и индексацией путей для поиска терминов, Журнал автоматизированного рассуждения, 9(2), 1992
  • П. Граф, Индексирование дерева подстановок, Proc. RTA, Lecture Notes in Computer Science 914, 1995
  • М. Стикель, Метод индексации пути для индексации терминов, Технический отчет 473, Центр искусственного интеллекта , SRI International , 1989
  • С. Шульц, Простая и эффективная классификация предложений с индексацией векторов признаков, Труды семинара IJCAR-2004 ESFOR, 2004
  • А. Рязанов и А. Воронков, Частично адаптивные кодовые деревья, Proc. JELIA, Lecture Notes in Artificial Intelligence 1919, 2000
  • Х. Ганзингер, Р. Нивенхейс и П. Нивела, Быстрое индексирование терминов с помощью кодированных контекстных деревьев, Журнал автоматизированного рассуждения, 32(2), 2004
  • А. Рязанов и А. Воронков, Эффективный поиск экземпляров с помощью стандартной и реляционной индексации путей, Информация и вычисления, 199(1–2), 2005
Получено с "https://en.wikipedia.org/w/index.php?title=Term_indexing&oldid=1187468825"