Чисті першопорядкові квазіaрні логіки з предикатами рівності
Вивчаються чистi першопорядковi квазіарні логіки однозначних та неоднозначних часткових предикатів. Основна увага приділена таким логікам із спеціальними предикатами рівності. Виділено чистi першопорядковi логіки з предикатами слабкої рівності та з предикатами строгої рівності. Описано мови та семан...
Saved in:
| Published in: | Проблеми програмування |
|---|---|
| Date: | 2017 |
| Main Authors: | , |
| Format: | Article |
| Language: | Ukrainian |
| Published: |
Інститут програмних систем НАН України
2017
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/144472 |
| 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: | Чисті першопорядкові квазіaрні логіки з предикатами рівності / М.С. Нікітченко, C.С. Шкільняк // Проблеми програмування. — 2017. — № 2. — С. 3-23. — Бібліогр.: 9 назв. — укр. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-144472 |
|---|---|
| record_format |
dspace |
| spelling |
Нікітченко, М.С. Шкільняк, C.С. 2018-12-24T17:42:25Z 2018-12-24T17:42:25Z 2017 Чисті першопорядкові квазіaрні логіки з предикатами рівності / М.С. Нікітченко, C.С. Шкільняк // Проблеми програмування. — 2017. — № 2. — С. 3-23. — Бібліогр.: 9 назв. — укр. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/144472 004.42:510.69 Вивчаються чистi першопорядковi квазіарні логіки однозначних та неоднозначних часткових предикатів. Основна увага приділена таким логікам із спеціальними предикатами рівності. Виділено чистi першопорядковi логіки з предикатами слабкої рівності та з предикатами строгої рівності. Описано мови та семантичні моделі цих логік, досліджено їх семантичні властивості, зокрема, властивості, пов’язані з предикатами рівності. Наведено властивості відношень логічного наслідку для множин формул. На базі цих властивостей для чистих першопорядкових логік з предикатами рівності побудовано низку числень секвенційного типу, для них доведено теореми коректності та повноти. Изучаются чистые первопорядковые логики однозначных и неоднозначных квазиарных предикатов. Эти логики являются программно-ориентированными логическими формализмами, отображающими такие свойства программ как частичность, недетерминизм, нефиксированную арность. Основное внимание уделено логикам со специальными предикатами равенства. Выделены чистые первопорядковые логики с предикатами слабого равенства и с предикатами строгого равенства. Описаны языки и семантические модели этих логик, исследованы их семантические свойства, в частности, свойства, связанные с предикатами равенства. Указаны свойства отношений логического следствия для множеств формул. На основе этих свойств для чистых первопорядковых логик с предикатами равенства построен ряд исчислений секвенциального типа, для них доказаны теоремы корректности и полноты. Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are studied. The main attention is paid to logics with special equality relations. Logics with weak equality and strong equality are defined, their properties are investigated. Languages of such logics and their interpetations are described. The following classes of interpretations (semantics) are identified: partial deterministic, non-deterministic, total deterministic, and total non-deterministic interpetations. Semantic properties of the proposed logics are investigated. Special attention is paid to consequence relations for sets of formulas. Based on the properties of these relations a number of calculi of sequent type is proposed. Basic rules of these calculi and corresponding closedness conditions are formulated; the procedure of sequent tree construction is described. For the proposed calculi correctness and completeness theorems are proved. The proof of completeness is based on the construction of countermodel for an unclosed path in the sequent tree. uk Інститут програмних систем НАН України Проблеми програмування Теоретичні та методологічні основи програмування Чисті першопорядкові квазіaрні логіки з предикатами рівності Чистые первопорядковые квазиарные логики с предикатами равенства Pure first-order quasiary logics with equality predicates Article published earlier |
| institution |
Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| collection |
DSpace DC |
| title |
Чисті першопорядкові квазіaрні логіки з предикатами рівності |
| spellingShingle |
Чисті першопорядкові квазіaрні логіки з предикатами рівності Нікітченко, М.С. Шкільняк, C.С. Теоретичні та методологічні основи програмування |
| title_short |
Чисті першопорядкові квазіaрні логіки з предикатами рівності |
| title_full |
Чисті першопорядкові квазіaрні логіки з предикатами рівності |
| title_fullStr |
Чисті першопорядкові квазіaрні логіки з предикатами рівності |
| title_full_unstemmed |
Чисті першопорядкові квазіaрні логіки з предикатами рівності |
| title_sort |
чисті першопорядкові квазіaрні логіки з предикатами рівності |
| author |
Нікітченко, М.С. Шкільняк, C.С. |
| author_facet |
Нікітченко, М.С. Шкільняк, C.С. |
| topic |
Теоретичні та методологічні основи програмування |
| topic_facet |
Теоретичні та методологічні основи програмування |
| publishDate |
2017 |
| language |
Ukrainian |
| container_title |
Проблеми програмування |
| publisher |
Інститут програмних систем НАН України |
| format |
Article |
| title_alt |
Чистые первопорядковые квазиарные логики с предикатами равенства Pure first-order quasiary logics with equality predicates |
| description |
Вивчаються чистi першопорядковi квазіарні логіки однозначних та неоднозначних часткових предикатів. Основна увага приділена таким логікам із спеціальними предикатами рівності. Виділено чистi першопорядковi логіки з предикатами слабкої рівності та з предикатами строгої рівності. Описано мови та семантичні моделі цих логік, досліджено їх семантичні властивості, зокрема, властивості, пов’язані з предикатами рівності. Наведено властивості відношень логічного наслідку для множин формул. На базі цих властивостей для чистих першопорядкових логік з предикатами рівності побудовано низку числень секвенційного типу, для них доведено теореми коректності та повноти.
Изучаются чистые первопорядковые логики однозначных и неоднозначных квазиарных предикатов. Эти логики являются программно-ориентированными логическими формализмами, отображающими такие свойства программ как частичность, недетерминизм, нефиксированную арность. Основное внимание уделено логикам со специальными предикатами равенства. Выделены чистые первопорядковые логики с предикатами слабого равенства и с предикатами строгого равенства. Описаны языки и семантические модели этих логик, исследованы их семантические свойства, в частности, свойства, связанные с предикатами равенства. Указаны свойства отношений логического следствия для множеств формул. На основе этих свойств для чистых первопорядковых логик с предикатами равенства построен ряд исчислений секвенциального типа, для них доказаны теоремы корректности и полноты.
Logics of quasiary predicates are program-oriented logics which aim to reflect such program properties as partiality, non-determinism, and non-fixed arity. In the paper, program-oriented logical formalisms – pure first-order logics of partial deterministic and non-deterministic predicates – are studied. The main attention is paid to logics with special equality relations. Logics with weak equality and strong equality are defined, their properties are investigated. Languages of such logics and their interpetations are described. The following classes of interpretations (semantics) are identified: partial deterministic, non-deterministic, total deterministic, and total non-deterministic interpetations. Semantic properties of the proposed logics are investigated. Special attention is paid to consequence relations for sets of formulas. Based on the properties of these relations a number of calculi of sequent type is proposed. Basic rules of these calculi and corresponding closedness conditions are formulated; the procedure of sequent tree construction is described. For the proposed calculi correctness and completeness theorems are proved. The proof of completeness is based on the construction of countermodel for an unclosed path in the sequent tree.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/144472 |
| citation_txt |
Чисті першопорядкові квазіaрні логіки з предикатами рівності / М.С. Нікітченко, C.С. Шкільняк // Проблеми програмування. — 2017. — № 2. — С. 3-23. — Бібліогр.: 9 назв. — укр. |
| work_keys_str_mv |
AT níkítčenkoms čistíperšoporâdkovíkvazíarnílogíkizpredikatamirívností AT škílʹnâkcs čistíperšoporâdkovíkvazíarnílogíkizpredikatamirívností AT níkítčenkoms čistyepervoporâdkovyekvaziarnyelogikispredikatamiravenstva AT škílʹnâkcs čistyepervoporâdkovyekvaziarnyelogikispredikatamiravenstva AT níkítčenkoms purefirstorderquasiarylogicswithequalitypredicates AT škílʹnâkcs purefirstorderquasiarylogicswithequalitypredicates |
| first_indexed |
2025-12-07T19:29:28Z |
| last_indexed |
2025-12-07T19:29:28Z |
| _version_ |
1850879003635744768 |