name: Нижние оценки и вопросы оптимальности для систем доказательств
keyword_list: резолюция по линейным равенствам нижние оценки OBDD цейтинские формулы Система доказательств
abstract: В диссертации изучаются системы доказательств, основанные на OBDD, сравниваются между собой разные версии таких систем доказательств, доказываются нижние оценки. Изучается сложность вывода цейтинских формул для произвольных графов, устанавливается связь с древесной шириной графа. Изучаются подсистемы резолюции над линейными уравнениями в поле из двух элементов, доказываются экспоненциальные нижние оценки на сложность вывода в этих подсистемах. Приводятся конструкции оптимальных эвристических и вероятностных аксепторов.
chairman_dissertation_council.name: Максим
chairman_dissertation_council.surname: Всемирнов
chairman_dissertation_council.patronymic: Александрович
chairman_dissertation_council.position: директор
chairman_dissertation_council.degree: Доктор физико-математических наук
chairman_dissertation_council.rank: Член-корреспондент РАН
chairman_dissertation_council.wos_research_id: J-3400-2013
chairman_dissertation_council.scopus_author_id: 23394353400
chairman_dissertation_council.rinc_id: 12091
chairman_dissertation_council.territory: РОССИЯ
organization_supervisor.name: Максим
organization_supervisor.surname: Всемирнов
organization_supervisor.patronymic: Александрович
organization_supervisor.position: директор
organization_supervisor.territory: РОССИЯ
rubrics.code: 27.03.45
rubrics.name: Теория вычислимости
rubrics.code: 27.03.55
rubrics.name: Теория доказательств
oecds.code: 01.01.PQ
oecds.name: MATHEMATICS
speciality_codes.name: Математическая логика, алгебра и теория чисел
speciality_codes.code: 01.01.06
opponents.fio: Верещагин Н.К.
opponents.scientific_degree: Доктор физико-математических наук
opponents.speciality_code: Математическая логика, алгебра и теория чисел
opponents.responsible_type: Оппонент
opponents.fio: Григорьев Д.Ю.
opponents.scientific_degree: Доктор физико-математических наук
opponents.speciality_code: Математическая логика, алгебра и теория чисел
opponents.responsible_type: Оппонент
opponents.fio: Разборов А.А.
opponents.scientific_degree: Доктор физико-математических наук
opponents.speciality_code: Математическая логика, алгебра и теория чисел
opponents.responsible_type: Оппонент
protection_organization.short_name: ПОМИ РАН
protection_organization.name: ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ САНКТ-ПЕТЕРБУРГСКОЕ ОТДЕЛЕНИЕ МАТЕМАТИЧЕСКОГО ИНСТИТУТА ИМ. В. А. СТЕКЛОВА РОССИЙСКОЙ АКАДЕМИИ НАУК
protection_organization.ogrn: 1037843013174
protection_organization.supervisor_name: МАКСИМ
protection_organization.supervisor_surname: ВСЕМИРНОВ
protection_organization.supervisor_patronymic: АЛЕКСАНДРОВИЧ
protection_organization.organization_type: Организация
protection_organization.okogu: Министерство науки и высшего образования Российской Федерации
protection_organization.okopf: Федеральные государственные бюджетные учреждения
author_organization.short_name: ПОМИ РАН
author_organization.name: ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ САНКТ-ПЕТЕРБУРГСКОЕ ОТДЕЛЕНИЕ МАТЕМАТИЧЕСКОГО ИНСТИТУТА ИМ. В. А. СТЕКЛОВА РОССИЙСКОЙ АКАДЕМИИ НАУК
author_organization.ogrn: 1037843013174
author_organization.supervisor_name: МАКСИМ
author_organization.supervisor_surname: ВСЕМИРНОВ
author_organization.supervisor_patronymic: АЛЕКСАНДРОВИЧ
author_organization.organization_type: Организация
author_organization.okogu: Министерство науки и высшего образования Российской Федерации
author_organization.okopf: Федеральные государственные бюджетные учреждения