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

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

Обзор

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

срок $q$ унифицирован с термином $t$ , т. е. существует замена $\theta$ , такой, что $q\theta$ = $t\theta$
срок $t$ является примером $q$ , т. е. существует замена $\theta$ , такой, что $q\theta$ = $t$
срок $t$ представляет собой обобщение $q$ , т. е. существует замена $\theta$ , такой, что $q$ = $t\theta$
пункт $q$ θ- предложение $t$ , т. е. существует замена $\theta$ , такой, что $q\theta$ является подмножеством/подмножеством $t$
пункт $q$ является θ-отнесенным к $t$ , т. е. существует замена $\theta$ , такой, что $t\theta$ является подмножеством/подмножеством $q$

Чаще всего мы действительно заинтересованы в поиске подходящего замены явно, вместе с полученными терминами $t$ ,а не просто в установлении существования таких замен.

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

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

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

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

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

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

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

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

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

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

Ссылки

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

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

П. Граф, Индексирование терминов, Конспекты лекций по информатике 1053, 1996 г. (немного устаревший обзор)
Р. Секар, И. В. Рамакришнан и А. Воронков, Индексирование терминов, в книге А. Робинсона и А. Воронкова, редакторы, Справочник по автоматическому рассуждению , том 2, 2001 г. (недавний обзор)
WW МакКьюн, Эксперименты с индексированием дерева дискриминации и индексированием путей для поиска терминов, Журнал автоматизированного рассуждения, 9 (2), 1992 г.
Граф П. Индексирование дерева замен. RTA, Конспекты лекций по информатике 914, 1995 г.
Стикель М., Метод индексации путей для терминов индексирования, Tech. Представитель 473, Центр искусственного интеллекта , SRI International , 1989 г.
С. Шульц, Простое и эффективное обобщение предложений с индексированием векторов признаков, Proc. семинара IJCAR-2004 ESFOR, 2004 г.
Рязанов А., Воронков А., Частично адаптивные деревья кодов, Учеб. ДЖЕЛИЯ, Конспекты лекций по искусственному интеллекту, 1919, 2000 г.
Х. Ганцингер, Р. Ньювенхейс и П. Нивела, Быстрое индексирование с помощью кодированных деревьев контекста, Журнал автоматизированного рассуждения, 32 (2), 2004 г.
А. Рязанов и А. Воронков, Эффективный поиск экземпляров с помощью индексации стандартных и реляционных путей, Информация и вычисления, 199 (1–2), 2005 г.

[1] Коломб, Роберт М. (1991). «Улучшение унификации в PROLOG посредством индексации предложений». Журнал логического программирования . 10 : 23–44. дои : 10.1016/0743-1066(91)90004-9 .

[2] Питер Граф. «Индексирование дерева замен» .1994.

[3] Джон В. Уилер; Гуарионекс Джордан. «Эмпирическое исследование индексации терминов в дарвиновской реализации модели эволюционного исчисления» .2004.п. 5.

[4] Кернер, Филипп; Леушель, Майкл; Барбоза, Жуан; Коста, Витор Сантос; Даль, Вероника; Эрменегильдо, Мануэль В.; Моралес, Хосе Ф.; Вилемакер, Ян; Диас, Дэниел; Абреу, Сальвадор; Чатто, Джованни (2022). «Пятьдесят лет Пролога и не только» . Теория и практика логического программирования . 22 (6): 776–858. дои : 10.1017/S1471068422000102 . hdl : 10174/33387 . ISSN 1471-0684 . В эту статью включен текст из этого источника, доступного по лицензии CC BY 4.0 .

[1]

[2]

[3]

[4]