Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення
Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих від...
Збережено в:
| Опубліковано в: : | Проблеми програмування |
|---|---|
| Дата: | 2019 |
| Автор: | |
| Формат: | Стаття |
| Мова: | Українська |
| Опубліковано: |
Інститут програмних систем НАН України
2019
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.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| _version_ | 1862538486228189184 |
|---|---|
| author | Шкільняк, О.С. |
| author_facet | Шкільняк, О.С. |
| citation_txt | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. |
| collection | DSpace DC |
| container_title | Проблеми програмування |
| description | Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо 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.
|
| first_indexed | 2025-11-24T15:05:05Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-161494 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Ukrainian |
| last_indexed | 2025-11-24T15:05:05Z |
| publishDate | 2019 |
| publisher | Інститут програмних систем НАН України |
| record_format | dspace |
| spelling | Шкільняк, О.С. 2019-12-11T21:44:09Z 2019-12-11T21:44:09Z 2019 Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. 1727-4907 DOI: https://doi.org/10.15407/pp2019.03.011 https://nasplib.isofts.kiev.ua/handle/123456789/161494 004.42:510.69 Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо 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. uk Інститут програмних систем НАН України Проблеми програмування Теоретичні та методологічні основи програмування Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення Отношения логического следствия в логиках частичных предикатов с композицией предикатного дополнения Relations of logical consequence in logics of partial predicates with composition of predicate complement Article published earlier |
| spellingShingle | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення Шкільняк, О.С. Теоретичні та методологічні основи програмування |
| title | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_alt | Отношения логического следствия в логиках частичных предикатов с композицией предикатного дополнения Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| title_full | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_fullStr | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_full_unstemmed | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_short | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_sort | відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| topic | Теоретичні та методологічні основи програмування |
| topic_facet | Теоретичні та методологічні основи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/161494 |
| work_keys_str_mv | AT škílʹnâkos vídnošennâlogíčnogonaslídkuvlogíkahčastkovihpredikatívzkompozicíêûpredikatnogodopovnennâ AT škílʹnâkos otnošeniâlogičeskogosledstviâvlogikahčastičnyhpredikatovskompozicieipredikatnogodopolneniâ AT škílʹnâkos relationsoflogicalconsequenceinlogicsofpartialpredicateswithcompositionofpredicatecomplement |