Отрывок: 2 Описание систем-аналогов Существует большое количество SMT-решателей, так что даже создаются специальные платформы для «соревнований» их между собой. Основное различие между решателями в списке поддерживаемых теорий. Многие из решателей поддерживают SMT-Lib (стандартизированный интерфейс взаимодействия между пользователем и решателем). Некоторые SMT-решатели работают только с бескванторными формулами, из-за сложности вычислений. 1.2.1 Z3 Z3 – SMT-решатель от Microsoft Research. Он о...
Название : Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения : вып. квалификац. работа по спец. "Фундаментальная информатика и информационные технологии"
Авторы/Редакторы : Савельев А. В.
Коварцев А. Н.
Министерство образования и науки Российской Федерации
Самарский национальный исследовательский университет им. С. П. Королева (Самарский университет)
Институт информатики
математики и электроники
Дата публикации : 2018
Библиографическое описание : Савельев, А. В. Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения : вып. квалификац. работа по спец. "Фундаментальная информатика и информационные технологии" / А. В. Савельев ; рук. работы А. Н. Коварцев ; М-во образования и науки Рос. Федерации, Самар. нац. исслед. ун-т им. С. П. Королева (Самар. ун-т), Ин-т информатики, математики и электроники, Фак-т инфо. - Самара, 2018. - on-line
Аннотация : Цель работы – разработать компилятор решающей функции для решателя в сигнатуре отношений сравнения.В процессе выполнения ВКР был разработан компилятор решающей функции для решателя в сигнатуре отношений сравнения, а в совокупности с другими подсистемами
URI (Унифицированный идентификатор ресурса) : http://repo.ssau.ru/handle/Vypusknye-kvalifikacionnye-raboty/Razrabotka-kompilyatora-reshaushei-funkcii-dlya-reshatelya-v-signature-otnoshenii-sravneniya-vyp-kvalifikac-rabota-po-spec-Fundamentalnaya-informatika-i-informacionnye-tehnologii-72938
Другие идентификаторы : RU\НТБ СГАУ\ВКР20180619144719
Ключевые слова: SMT-формула
компилятор решающей функции
решающая функция
сигнатура отношений сравнения
Располагается в коллекциях: Выпускные квалификационные работы




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