Отрывок: 2 Описание систем-аналогов Существует большое количество SMT-решателей, так что даже создаются специальные платформы для «соревнований» их между собой. Основное различие между решателями в списке поддерживаемых теорий. Многие из решателей поддерживают SMT-Lib (стандартизированный интерфейс взаимодействия между пользователем и решателем). Некоторые SMT-решатели работают только с бескванторными формулами, из-за сложности вычислений. 1.2.1 Z3 Z3 – SMT-решатель от Microsoft Research. Он о...
Название : Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения
Авторы/Редакторы : Савельев А. В.
Коварцев А. Н.
Министерство образования и науки Российской Федерации
Самарский национальный исследовательский университет им. С. П. Королева (Самарский университет)
Институт информатики
математики и электроники
Дата публикации : 2018
Библиографическое описание : Савельев, А. В. Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения : вып. квалификац. работа по спец. "Фундаментальная информатика и информационные технологии" / А. В. Савельев ; рук. работы А. Н. Коварцев ; М-во образования и науки Рос. Федерации, Самар. нац. исслед. ун-т им. С. П. Королева (Самар. ун-т), Ин-т информатики, математики и электроники, Фак-т инфо. - Самара, 2018. - on-line
Аннотация : Цель работы – разработать компилятор решающей функции для решателя в сигнатуре отношений сравнения.В процессе выполнения ВКР был разработан компилятор решающей функции для решателя в сигнатуре отношений сравнения, а в совокупности с другими подсистемами – сам решатель, позволяющий проверять на выполнимость SMT-формулы. Подсистема-компилятор разработана на языке программирования TURBO-Пролог.
Другие идентификаторы : RU\НТБ СГАУ\ВКР20180619144719
Ключевые слова: SMT-формула
сигнатура отношений сравнения
компилятор решающей функции
решающая функция
Располагается в коллекциях: Выпускные квалификационные работы

Файлы этого ресурса:
Файл Размер Формат  
Савельев_Александр_Владиславович_Разработка_компилятора_решающей_функции.pdf1.19 MBAdobe PDFПросмотреть/Открыть  
Показать полное описание ресурса Просмотр статистики
Поделиться:



Все ресурсы в архиве электронных ресурсов защищены авторским правом, все права сохранены.