Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення
Vernadsky National Library of Ukraine
Переглянути архів Інформація| Поле | Співвідношення | |
| Title |
Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення
|
|
| Creator |
Шкільняк, О.С.
Касьянюк, В.С. Малютенко, Л.М. |
|
| Subject |
Теоретичні та методологічні основи програмування
|
|
| 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. |
|
| Date |
2018-12-24T17:44:52Z
2018-12-24T17:44:52Z 2017 |
|
| Type |
Article
|
|
| Identifier |
Композиційно-номінативні модальні логіки немонотонних часткових предикатів та їх числення / О.С. Шкільняк, В.С. Касьянюк, Л.М. Малютенко // Проблеми програмування. — 2017. — № 2. — С. 24-39. — Бібліогр.: 9 назв. — укр.
1727-4907 http://dspace.nbuv.gov.ua/handle/123456789/144473 004.42:510.69 |
|
| Language |
uk
|
|
| Relation |
Проблеми програмування
|
|
| Publisher |
Інститут програмних систем НАН України
|
|