Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення
Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих від...
Збережено в:
| Дата: | 2019 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Ukrainian |
| Опубліковано: |
Інститут програмних систем НАН України
2019
|
| Назва видання: | Проблеми програмування |
| Теми: | |
| Онлайн доступ: | http://dspace.nbuv.gov.ua/handle/123456789/161494 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
irk-123456789-161494 |
|---|---|
| record_format |
dspace |
| spelling |
irk-123456789-1614942019-12-12T01:26:39Z Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення Шкільняк, О.С. Теоретичні та методологічні основи програмування Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої наявності, наведено властивості декомпозиції формул та елімінації кванторів. В работе исследованы программно-ориентированные логики частичных предикатов, названные LC. Характерной их особенностью является наличие новой операции (композиции) предикатного дополнения. Операции такого типа используются в различных вариантах программных логик Флойда-Хоара с частичными перед- и после-условиями. Описаны композиционные алгебры и языки LC. Для предложенных отношений описаны условия их гарантированного наличия, приведены свойства декомпозиции формул и свойства элиминации кванторов. In this paper we study software-oriented logics of partial predicates with new special non-monotonic operation (composition) of the predicate complement. We denote these logics by LC and composition of the predicate complement by . Such operations are used in various versions of the Floyd-Hoare program logic with partial pre- and post-conditions. We describe first order composition algebras and LC languages. For the introduced relations, we describe the conditions for their guaranteed presence, the decomposition conditions for formulas and the properties of quantifier elimination. 2019 Article Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. 1727-4907 DOI: https://doi.org/10.15407/pp2019.03.011 http://dspace.nbuv.gov.ua/handle/123456789/161494 004.42:510.69 uk Проблеми програмування Інститут програмних систем НАН України |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| language |
Ukrainian |
| topic |
Теоретичні та методологічні основи програмування Теоретичні та методологічні основи програмування |
| spellingShingle |
Теоретичні та методологічні основи програмування Теоретичні та методологічні основи програмування Шкільняк, О.С. Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення Проблеми програмування |
| description |
Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих відношень, встановлено співвідношення між ними. Для відношень типів |=T та |=F доведено теорему про елімінацію умов невизначеності. Для запропонованих відношень описано умови їх гарантованої наявності, наведено властивості декомпозиції формул та елімінації кванторів. |
| format |
Article |
| author |
Шкільняк, О.С. |
| author_facet |
Шкільняк, О.С. |
| author_sort |
Шкільняк, О.С. |
| title |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_short |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_full |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_fullStr |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_full_unstemmed |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_sort |
відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| publisher |
Інститут програмних систем НАН України |
| publishDate |
2019 |
| topic_facet |
Теоретичні та методологічні основи програмування |
| url |
http://dspace.nbuv.gov.ua/handle/123456789/161494 |
| citation_txt |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. |
| series |
Проблеми програмування |
| work_keys_str_mv |
AT škílʹnâkos vídnošennâlogíčnogonaslídkuvlogíkahčastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ |
| first_indexed |
2023-06-10T11:11:35Z |
| last_indexed |
2023-06-10T11:11:35Z |
| _version_ |
1796154679550279680 |