Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення
Досліджено нові програмно-орієнтовані логічні формалізми модального типу – композиційно-номінативні модальні логіки немонотонних часткових предикатів. Описано семантичні моделі та мови цих логік, розглянуто основні семантичні властивості. Введено відношення наслідку для формул у стані, описано власт...
Saved in:
| Published in: | Проблеми програмування |
|---|---|
| Date: | 2017 |
| Main Authors: | , , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут програмних систем НАН України
2017
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/144473 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Проблеми програмування. — 2017. — № 2. — С. 24-39. — Бібліогр.: 9 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-144473 |
|---|---|
| record_format |
dspace |
| spelling |
Шкільняк, О.С. Касьянюк, В.С. Малютенко, Л.М. 2018-12-24T17:44:52Z 2018-12-24T17:44:52Z 2017 Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Проблеми програмування. — 2017. — № 2. — С. 24-39. — Бібліогр.: 9 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/144473 004.42:510.69 Досліджено нові програмно-орієнтовані логічні формалізми модального типу – композиційно-номінативні модальні логіки немонотонних часткових предикатів. Описано семантичні моделі та мови цих логік, розглянуто основні семантичні властивості. Введено відношення наслідку для формул у стані, описано властивості відношення логічного наслідку для множин специфікованих станами формул. На цій основі для загальних i темпоральних модальних логік немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них доведено теореми коректності й повноти. Исследованы новые программно-ориентированные логические формализмы модального типа – композиционно-номинативные модальные логики немонотонных частичных предикатов. Описаны семантические модели и языки этих логик, рассмотрено взаимодействие модальных композиций с реноминациями и кванторами. Введено отношение следствия для формул в данном состоянии, оно обобщено до отношения логического следствия для множеств специфицированных состояниями формул. Для общих и темпоральных модальных логик немонотонных предикатов построены исчисления секвенциального типа. Описаны разновидности этих исчислений, для них доказаны теорема корректности и теорема о существовании контрмодели для незамкнутого пути в секвенциальном дереве. На основе теоремы о контрмодели доказана теорема полноты. We consider new program-oriented logical formalisms of modal type – pure first-order composition nominative modal logics of partial predicates without monotonicity restriction. For such logics we specify semantic models and languages and investigate interactions of modal compositions with renominations and quantifiers. A consequence relation for two formulas in a given state is introduced and generalized to a logical consequence relation for two sets of formulas specified with states. We describe properties of a logical consequence relation for sets of formulas specified with states and properties of modalities elimination for various reachability relations. Sequent type calculi are proposed for general transitional and temporal modal logics of non-monotone predicates. We define various types of the calculi for different reachability relations and specify their basic sequent forms and sequent closure conditions. We give a step-by-step description of a deriving process (building of a sequent tree) by the introduced calculi. For these calculi we prove the soundness theorem and the theorem about existence of a counter-model for a non-closed path in a sequent tree. The counter-model is obtained using the Hintikka sets method. The proof of the completeness theorem is based on the theorem about existence of a counter-model. uk Інститут програмних систем НАН України Проблеми програмування Теоретичні та методологічні основи програмування Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення Композиционно-номинативные модальные логики немонотонных частичных предикатов и их исчисления Composition nominative modal logics of partial non-monotone predicates and their calculi 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 |
2017 |
| language |
Ukrainian |
| container_title |
Проблеми програмування |
| publisher |
Інститут програмних систем НАН України |
| format |
Article |
| title_alt |
Композиционно-номинативные модальные логики немонотонных частичных предикатов и их исчисления Composition nominative modal logics of partial non-monotone predicates and their calculi |
| description |
Досліджено нові програмно-орієнтовані логічні формалізми модального типу – композиційно-номінативні модальні логіки немонотонних часткових предикатів. Описано семантичні моделі та мови цих логік, розглянуто основні семантичні властивості. Введено відношення наслідку для формул у стані, описано властивості відношення логічного наслідку для множин специфікованих станами формул. На цій основі для загальних i темпоральних модальних логік немонотонних предикатів побудовано числення секвенційного типу. Описано різновиди цих числень, для них доведено теореми коректності й повноти.
Исследованы новые программно-ориентированные логические формализмы модального типа – композиционно-номинативные модальные логики немонотонных частичных предикатов. Описаны семантические модели и языки этих логик, рассмотрено взаимодействие модальных композиций с реноминациями и кванторами. Введено отношение следствия для формул в данном состоянии, оно обобщено до отношения логического следствия для множеств специфицированных состояниями формул. Для общих и темпоральных модальных логик немонотонных предикатов построены исчисления секвенциального типа. Описаны разновидности этих исчислений, для них доказаны теорема корректности и теорема о существовании контрмодели для незамкнутого пути в секвенциальном дереве. На основе теоремы о контрмодели доказана теорема полноты.
We consider new program-oriented logical formalisms of modal type – pure first-order composition nominative modal logics of partial predicates without monotonicity restriction. For such logics we specify semantic models and languages and investigate interactions of modal compositions with renominations and quantifiers. A consequence relation for two formulas in a given state is introduced and generalized to a logical consequence relation for two sets of formulas specified with states. We describe properties of a logical consequence relation for sets of formulas specified with states and properties of modalities elimination for various reachability relations. Sequent type calculi are proposed for general transitional and temporal modal logics of non-monotone predicates. We define various types of the calculi for different reachability relations and specify their basic sequent forms and sequent closure conditions. We give a step-by-step description of a deriving process (building of a sequent tree) by the introduced calculi. For these calculi we prove the soundness theorem and the theorem about existence of a counter-model for a non-closed path in a sequent tree. The counter-model is obtained using the Hintikka sets method. The proof of the completeness theorem is based on the theorem about existence of a counter-model.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/144473 |
| citation_txt |
Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Проблеми програмування. — 2017. — № 2. — С. 24-39. — Бібліогр.: 9 назв. — укр. |
| work_keys_str_mv |
AT škílʹnâkos kompozicíinonomínativnímodalʹnílogíkinemonotonnihčastkovihpredikatívtaíhčislennâ AT kasʹânûkvs kompozicíinonomínativnímodalʹnílogíkinemonotonnihčastkovihpredikatívtaíhčislennâ AT malûtenkolm kompozicíinonomínativnímodalʹnílogíkinemonotonnihčastkovihpredikatívtaíhčislennâ AT škílʹnâkos kompozicionnonominativnyemodalʹnyelogikinemonotonnyhčastičnyhpredikatoviihisčisleniâ AT kasʹânûkvs kompozicionnonominativnyemodalʹnyelogikinemonotonnyhčastičnyhpredikatoviihisčisleniâ AT malûtenkolm kompozicionnonominativnyemodalʹnyelogikinemonotonnyhčastičnyhpredikatoviihisčisleniâ AT škílʹnâkos compositionnominativemodallogicsofpartialnonmonotonepredicatesandtheircalculi AT kasʹânûkvs compositionnominativemodallogicsofpartialnonmonotonepredicatesandtheircalculi AT malûtenkolm compositionnominativemodallogicsofpartialnonmonotonepredicatesandtheircalculi |
| first_indexed |
2025-12-07T13:34:00Z |
| last_indexed |
2025-12-07T13:34:00Z |
| _version_ |
1850856639944458240 |