Задача проверки Т-выполнимости для логического языка VL1 системы VRS

Задача проверки Т-выполнимости для логического языка VL1 системы VRS

В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования, которая представлена в системе верификации требований VRS. Дается...

Повний опис

Збережено в:
Бібліографічні деталі
Видавець:Інститут програмних систем НАН України
Дата:2012
Автор: Тимофеев, В.Г.
Мова:Russian
Опубліковано: Інститут програмних систем НАН України 2012
Назва видання:Проблеми програмування
Теми:
Формальні методи програмування
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/86610
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Цитувати:Задача проверки Т-выполнимости для логического языка VL1 системы VRS / В.Г. Тимофеев // Проблеми програмування. — 2012. — № 2-3. — С. 251-259. — Бібліогр.: 21 назв. — рос.

Репозиторії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-86610
record_format dspace
spelling irk-123456789-866102015-09-24T03:02:28Z Задача проверки Т-выполнимости для логического языка VL1 системы VRS Тимофеев, В.Г. Формальні методи програмування В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования, которая представлена в системе верификации требований VRS. Дается формализация логического языка, используемого в VRS для проведения формальных рассуждений, и показывается разрешимость проблемы выполнимости формул в этом языке. Обсуждаются особенности применения используемых методов, и описывается альтернативный алгоритм поиска выполнимой конъюнкции, основанный на множественном представлении операций в формулах. In this paper we give a short introduction to the satisfiability modulo theories (SMT) problem and demonstrate how the methods developed in the SMT research field can be applied in the requirement verification tool VRS, which supports insertion modelling methodology. We formalize the logical language VL1 used for formal reasoning in VRS and justify decidability of satisfiability problem in that language. Besides we discuss the context of the problem being solved and indicate possible methods that can be used on different stages of solution. Finally, we present a satisfiable conjunction search method, which is based on a set-representation of logical connectives in formulas. 2012 Задача проверки Т-выполнимости для логического языка VL1 системы VRS / В.Г. Тимофеев // Проблеми програмування. — 2012. — № 2-3. — С. 251-259. — Бібліогр.: 21 назв. — рос. 1727-4907 http://dspace.nbuv.gov.ua/handle/123456789/86610 004.02 ru Проблеми програмування Інститут програмних систем НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Russian
topic Формальні методи програмування
Формальні методи програмування
spellingShingle Формальні методи програмування
Формальні методи програмування
Тимофеев, В.Г.
Задача проверки Т-выполнимости для логического языка VL1 системы VRS
Проблеми програмування
description В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования, которая представлена в системе верификации требований VRS. Дается формализация логического языка, используемого в VRS для проведения формальных рассуждений, и показывается разрешимость проблемы выполнимости формул в этом языке. Обсуждаются особенности применения используемых методов, и описывается альтернативный алгоритм поиска выполнимой конъюнкции, основанный на множественном представлении операций в формулах.
author Тимофеев, В.Г.
author_facet Тимофеев, В.Г.
author_sort Тимофеев, В.Г.
title Задача проверки Т-выполнимости для логического языка VL1 системы VRS
title_short Задача проверки Т-выполнимости для логического языка VL1 системы VRS
title_full Задача проверки Т-выполнимости для логического языка VL1 системы VRS
title_fullStr Задача проверки Т-выполнимости для логического языка VL1 системы VRS
title_full_unstemmed Задача проверки Т-выполнимости для логического языка VL1 системы VRS
title_sort задача проверки т-выполнимости для логического языка vl1 системы vrs
publisher Інститут програмних систем НАН України
publishDate 2012
topic_facet Формальні методи програмування
url http://dspace.nbuv.gov.ua/handle/123456789/86610
citation_txt Задача проверки Т-выполнимости для логического языка VL1 системы VRS / В.Г. Тимофеев // Проблеми програмування. — 2012. — № 2-3. — С. 251-259. — Бібліогр.: 21 назв. — рос.
series Проблеми програмування
work_keys_str_mv AT timofeevvg zadačaproverkitvypolnimostidlâlogičeskogoâzykavl1sistemyvrs
first_indexed 2023-10-18T19:33:45Z
last_indexed 2023-10-18T19:33:45Z
_version_ 1796147298672050176

Схожі ресурси