Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення
Досліджено нові програмно-орієнтовані логіки часткових предикатів з операцією (композицією) предикатного доповнення, такі логіки названо LC. Для першопорядкових LC запропоновано низку відношень логічного наслідку та відношень логічного наслідку за умови невизначеності. Досліджено властивості цих від...
Gespeichert in:
| Veröffentlicht in: | Проблеми програмування |
|---|---|
| Datum: | 2019 |
| 1. Verfasser: | |
| Format: | Artikel |
| Sprache: | Ukrainian |
| Veröffentlicht: |
Інститут програмних систем НАН України
2019
|
| Schlagworte: | |
| Online Zugang: | https://nasplib.isofts.kiev.ua/handle/123456789/161494 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Zitieren: | Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-161494 |
|---|---|
| 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 |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| spellingShingle |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення Шкільняк, О.С. Теоретичні та методологічні основи програмування |
| title_short |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_full |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_fullStr |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_full_unstemmed |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| title_sort |
відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення |
| author |
Шкільняк, О.С. |
| author_facet |
Шкільняк, О.С. |
| topic |
Теоретичні та методологічні основи програмування |
| topic_facet |
Теоретичні та методологічні основи програмування |
| publishDate |
2019 |
| language |
Ukrainian |
| container_title |
Проблеми програмування |
| publisher |
Інститут програмних систем НАН України |
| format |
Article |
| title_alt |
Отношения логического следствия в логиках частичных предикатов с композицией предикатного дополнения Relations of logical consequence in logics of partial predicates with composition of predicate complement |
| 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.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/161494 |
| fulltext |
|
| citation_txt |
Відношення логічного наслідку в логіках часткових предикатів з композицією предикатного доповнення / О.С. Шкільняк // Проблеми програмування. — 2019. — № 3. — С. 11-27. — Бібліогр.: 10 назв. — укр. |
| 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 |
| first_indexed |
2025-11-24T15:05:05Z |
| last_indexed |
2025-11-24T15:05:05Z |
| _version_ |
1850847397688639488 |