Отрывок: 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.spatialSMT-формулаru
dc.coverage.spatialсигнатура отношений сравненияru
dc.coverage.spatialкомпилятор решающей функцииru
dc.coverage.spatialрешающая функцияru
dc.creatorСавельев А. В.ru
dc.date.issued2018ru
dc.identifierRU\НТБ СГАУ\ВКР20180619144719ru
dc.identifier.citationСавельев, А. В. Разработка компилятора решающей функции для решателя в сигнатуре отношений сравнения : вып. квалификац. работа по спец. "Фундаментальная информатика и информационные технологии" / А. В. Савельев ; рук. работы А. Н. Коварцев ; М-во образования и науки Рос. Федерации, Самар. нац. исслед. ун-т им. С. П. Королева (Самар. ун-т), Ин-т информатики, математики и электроники, Фак-т инфо. - Самара, 2018. - on-lineru
dc.description.abstractЦель работы – разработать компилятор решающей функции для решателя в сигнатуре отношений сравнения.В процессе выполнения ВКР был разработан компилятор решающей функции для решателя в сигнатуре отношений сравнения, а в совокупности с другими подсистемами – сам решатель, позволяющий проверять на выполнимость SMT-формулы. Подсистема-компилятор разработана на языке программирования TURBO-Пролог.ru
dc.format.extentЭлектрон. дан. (1 файл : 1,2 Мб)ru
dc.titleРазработка компилятора решающей функции для решателя в сигнатуре отношений сравненияru
dc.typeTextru
dc.subject.rugasnti50.01ru
dc.subject.udc004.9ru
dc.textpart2 Описание систем-аналогов Существует большое количество SMT-решателей, так что даже создаются специальные платформы для «соревнований» их между собой. Основное различие между решателями в списке поддерживаемых теорий. Многие из решателей поддерживают SMT-Lib (стандартизированный интерфейс взаимодействия между пользователем и решателем). Некоторые SMT-решатели работают только с бескванторными формулами, из-за сложности вычислений. 1.2.1 Z3 Z3 – SMT-решатель от Microsoft Research. Он о...-
Располагается в коллекциях: Выпускные квалификационные работы




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