Исследовательская группа
Лаборатория языковых инструментов
Индексация с помощью деревьев подстановок
April 8
Эффективность систем автоматического доказательства теорем в решающей степени зависит от скорости основных операций поиска, таких как поиск выражений, которые можно унифицировать (уточнить, обобщить) с заданным выражением.
Первая часть доклада посвящена методу индексации, который позволяет представлять набор подстановок в виде компактной древовидной структуры данных.
Во второй части доклада обсуждаются теоретические основы и реализация нескольких операций для работы с этой структурой данных, таких как поиск подстановки, объединение, вставка и удаление.
Материалы к докладу:
Peter Graf. Substitution tree indexing // International Conference on Rewriting Techniques and Applications, 1995.
Докладчик: Петр Лозов