Задача проверки Т-выполнимости для логического языка VL1 системы VRS
В данной работе дается короткое введение в задачу проверки T-выполнимости формул относительно логических теорий, и показывается, что разработанные методы решения этой задачи могут применяться в технологии инсерционного моделирования, которая представлена в системе верификации требований VRS. Дается...
Збережено в:
| Опубліковано в: : | Проблеми програмування |
|---|---|
| Дата: | 2012 |
| Автор: | |
| Мова: | Російська |
| Опубліковано: |
Інститут програмних систем НАН України
2012
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/86610 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Задача проверки Т-выполнимости для логического языка VL1 системы VRS / В.Г. Тимофеев // Проблеми програмування. — 2012. — № 2-3. — С. 251-259. — Бібліогр.: 21 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862720072337850368 |
|---|---|
| author | Тимофеев, В.Г. |
| author_facet | Тимофеев, В.Г. |
| citation_txt | Задача проверки Т-выполнимости для логического языка VL1 системы VRS / В.Г. Тимофеев // Проблеми програмування. — 2012. — № 2-3. — С. 251-259. — Бібліогр.: 21 назв. — рос. |
| collection | DSpace DC |
| container_title | Проблеми програмування |
| description | В данной работе дается короткое введение в задачу проверки 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.
|
| first_indexed | 2025-12-07T18:23:25Z |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-86610 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Russian |
| last_indexed | 2025-12-07T18:23:25Z |
| publishDate | 2012 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Тимофеев, В.Г. 2015-09-23T16:25:10Z 2015-09-23T16:25:10Z 2012 Задача проверки Т-выполнимости для логического языка VL1 системы VRS / В.Г. Тимофеев // Проблеми програмування. — 2012. — № 2-3. — С. 251-259. — Бібліогр.: 21 назв. — рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/86610 004.02 В данной работе дается короткое введение в задачу проверки 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. ru Інститут програмних систем НАН України Проблеми програмування Формальні методи програмування Задача проверки Т-выполнимости для логического языка VL1 системы VRS published earlier |
| spellingShingle | Задача проверки Т-выполнимости для логического языка VL1 системы VRS Тимофеев, В.Г. Формальні методи програмування |
| title | Задача проверки Т-выполнимости для логического языка VL1 системы VRS |
| title_full | Задача проверки Т-выполнимости для логического языка VL1 системы VRS |
| title_fullStr | Задача проверки Т-выполнимости для логического языка VL1 системы VRS |
| title_full_unstemmed | Задача проверки Т-выполнимости для логического языка VL1 системы VRS |
| title_short | Задача проверки Т-выполнимости для логического языка VL1 системы VRS |
| title_sort | задача проверки т-выполнимости для логического языка vl1 системы vrs |
| topic | Формальні методи програмування |
| topic_facet | Формальні методи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/86610 |
| work_keys_str_mv | AT timofeevvg zadačaproverkitvypolnimostidlâlogičeskogoâzykavl1sistemyvrs |