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

Унификация посредством поиска путей с контекстно-свободными ограничениями в графе

Задача унификации — определить, являются ли два терма частными случаями друг друга. Унификация используется в логических языках, при выводе типов, в системах интерактивного доказательства теорем и многих других задачах. Синтаксическая унификация может быть выражена как поиск путей с контекстно-свободными ограничениями в некотором графе. При этом путь тесно связан с доказательством унифицируемости термов. В докладе поговорим о том, как построить граф по задаче синтаксической унификации первого порядка, какой язык использовать в качестве ограничений и как доказать, что данные термы унифицируемы.

Докладчик: Екатерина Вербицкая

Материалы

Choppella, Venkatesh, and Christopher T. Haynes. "Source-tracking unification." Information and Computation 201, no. 2 (2005): 121-159.

Семинар пройдет онлайн 16 ноября в 17:30, ссылка Google meet: https://meet.google.com/myu-dhmz-gvu