Лаборатория языковых инструментов

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

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

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

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

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

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