Институт системного программирования Роcсийской академии наук


Современные алгоритмические проблемы дискретной математики

Начало проекта – 2014 год.

Проблема защиты информации в облачных вычислениях намного сложнее тех задач защиты информации, которые решаются известными криптографическими средствами. В 2010 г. в работе ван Дейка и др. была рассмотрена математическая модель облачных вычислений над конфиденциальными данными. Доказано, что уже в случае двух пользователей защита информации невозможна. Возникает научная проблема выделения тех моделей облачных вычислений и вычислительных задач, для которых возможна защита информации.

Впервые задачу унификации исследовал Дж. Робинсон в рамках разработки метода резолюций для систем автоматического доказательства теорем. В дальнейшем метод резолюций послужил отправной точкой для разработки концепции логического программирования, и алгоритмы унификации фактически стали основным средством вычисления логических программ. За прошедшие годы задача унификации была детально исследована. Было обнаружено, что унификация, помимо логического программирования, может быть использована при разработке систем автоматического доказательства теорем, обработке текстов естественных и формальных языков, построении систем переписывания термов. Был разработан широкий спектр эффективных алгоритмов унификации, имеющих почти линейную сложность, а также были найдены подходящие структуры данных для практической реализации этих алгоритмов.

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


Проект выполняется в рамках программы фундаментальных исследований Отделения Математических Наук РАН «Современные проблемы теоретической математики».

Исполнитель

Теоретическая информатика

Перейти к списку всех проектов