JetBrains Research — наука, меняющая мир

Семинар по индексации с помощью деревьев подстановок

Эффективность систем автоматического доказательства теорем в решающей степени зависит от скорости основных операций поиска, таких как поиск выражений, которые можно унифицировать (уточнить, обобщить) с заданным выражением.

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

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

Материалы к докладу:

Peter Graf. Substitution tree indexing // International Conference on Rewriting Techniques and Applications, 1995.

Докладчик: Петр Лозов

08.04.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28