Секвенційні числення першопорядкових логік часткових предикатів з розширеними реномінаціями та композицією предикатного доповнення

• Опубліковано в: : Проблеми програмування
• Дата: 2020
• Автори: Нікітченко, М.С., Шкільняк, О.С., Шкільняк, С.С.
• Формат: Стаття
• Мова: Ukrainian
• Опубліковано: Інститут програмних систем НАН України 2020
• Теми: Теоретичні та методологічні основи програмування
• Онлайн доступ: https://nasplib.isofts.kiev.ua/handle/123456789/180464
• Назва журналу: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Цитувати: Секвенційні числення першопорядкових логік часткових предикатів з розширеними реномінаціями та композицією предикатного доповнення / М.С. Нікітченко, О.С. Шкільняк, С.С. Шкільняк // Проблеми програмування. — 2020. — № 2-3. — С. 182-197. — Бібліогр.: 12 назв. — укр.

Досліджено нові класи програмно-орієнтованих логік – чисті першопорядкові логіки часткових квазіарних предикатів з розширеними реномінаціями та композицією предикатного доповнення. Описано відношення логічного наслідку в таких логіках, для цих відношень побудовано числення секвенційного типу. Наведено базові секвенційні форми цих числень та умови замкненості секвенцій. Для пропонованих числень доведено теореми коректності, теореми про існування контрмоделей та теореми повноти. Исследованы новые классы программно-ориентированных логик – чистые первопорядковые логики частичных квазиарных предикатов с расширенными реноминациями и композицией предикатного дополнения. Описаны отношення логического следствия в таких логиках, для этих отношений построены исчисления секвенциального типа. Приведены базовые секвенциальные формы этих исчислений и условия замкнутости секвенций. Для предложенных исчислений доказаны теоремы корректности, теоремы о существовании контрмоделей и теоремы полноты. We study new classes of program-oriented logical formalisms – pure first-order logics of quasiary predicates with extended renominations and a composition of predicate complement. For these logics, various logical consequence relations are specified and corresponding calculi of sequent type are constructed. We define basic sequent forms for the specified calculi and closeness conditions. The soundness, completeness, and counter-model existence theorems are proved for the introduced calculi