Отрывок: 2 Описание систем-аналогов Существует большое количество SMT-решателей, так что даже создаются специальные платформы для «соревнований» их между собой. Основное различие между решателями в списке поддерживаемых теорий. Многие из решателей поддерживают SMT-Lib (стандартизированный интерфейс взаимодействия между пользователем и решателем). Некоторые SMT-решатели работают только с бескванторными формулами, из-за сложности вычислений. 1.2.1 Z3 Z3 – SMT-решатель от Microsoft Research. Он о...
Полная запись метаданных
Поле DC | Значение | Язык |
---|---|---|
dc.contributor.author | Савельев А. В. | ru |
dc.contributor.author | Коварцев А. Н. | ru |
dc.contributor.author | Министерство образования и науки Российской Федерации | ru |
dc.contributor.author | Самарский национальный исследовательский университет им. С. П. Королева (Самарский университет) | ru |
dc.contributor.author | Институт информатики | ru |
dc.contributor.author | математики и электроники | ru |
dc.coverage.spatial | SMT-формула | ru |
dc.coverage.spatial | сигнатура отношений сравнения | ru |
dc.coverage.spatial | компилятор решающей функции | ru |
dc.coverage.spatial | решающая функция | ru |
dc.creator | Савельев А. В. | ru |
dc.date.issued | 2018 | ru |
dc.identifier | RU\НТБ СГАУ\ВКР20180619144719 | ru |
dc.identifier.citation | Савельев, А. В. Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения : вып. квалификац. работа по спец. "Фундаментальная информатика и информационные технологии" / А. В. Савельев ; рук. работы А. Н. Коварцев ; М-во образования и науки Рос. Федерации, Самар. нац. исслед. ун-т им. С. П. Королева (Самар. ун-т), Ин-т информатики, математики и электроники, Фак-т инфо. - Самара, 2018. - on-line | ru |
dc.description.abstract | Цель работы – разработать компилятор решающей функции для решателя в сигнатуре отношений сравнения.В процессе выполнения ВКР был разработан компилятор решающей функции для решателя в сигнатуре отношений сравнения, а в совокупности с другими подсистемами – сам решатель, позволяющий проверять на выполнимость SMT-формулы. Подсистема-компилятор разработана на языке программирования TURBO-Пролог. | ru |
dc.format.extent | Электрон. дан. (1 файл : 1,2 Мб) | ru |
dc.title | Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения | ru |
dc.type | Text | ru |
dc.subject.rugasnti | 50.01 | ru |
dc.subject.udc | 004.9 | ru |
dc.textpart | 2 Описание систем-аналогов Существует большое количество SMT-решателей, так что даже создаются специальные платформы для «соревнований» их между собой. Основное различие между решателями в списке поддерживаемых теорий. Многие из решателей поддерживают SMT-Lib (стандартизированный интерфейс взаимодействия между пользователем и решателем). Некоторые SMT-решатели работают только с бескванторными формулами, из-за сложности вычислений. 1.2.1 Z3 Z3 – SMT-решатель от Microsoft Research. Он о... | - |
Располагается в коллекциях: | Выпускные квалификационные работы |
Файлы этого ресурса:
Файл | Размер | Формат | |
---|---|---|---|
Савельев_Александр_Владиславович_Разработка_компилятора_решающей_функции.pdf | 1.19 MB | Adobe PDF | Просмотреть/Открыть |
Показать базовое описание ресурса
Просмотр статистики
Поделиться:
Все ресурсы в архиве электронных ресурсов защищены авторским правом, все права сохранены.