Секвенційні числення логік безкванторно-функціональних рівнів

• Опубліковано в: : Штучний інтелект
• Дата: 2016
• Автори: Шкільняк, С.С., Волковицький, Д.Б.
• Формат: Стаття
• Мова: Українська
• Опубліковано: Інститут проблем штучного інтелекту МОН України та НАН України 2016
• Теми: Теорія та засоби обчислювального інтелекту
• Онлайн доступ: https://nasplib.isofts.kiev.ua/handle/123456789/132088
• Назва журналу: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Цитувати: Секвенційні числення логік безкванторно-функціональних рівнів / С.С. Шкільняк, Д.Б. Волковицький // Штучний інтелект. — 2016. — № 4. — С. 50-62. — Бібліогр.: 5 назв. — укр.

Для безкванторно-функціональних логік та їх різновидів зі слабкою рівністю та строгою рівністю побудовано числення секвенційного типу. Такі числення формалізують відношення неспростовнісного, істиннісного, хибнісного та сильного логічного наслідку. Для цих числень доведено теореми коректності й повноти. На базі теорем повноти отримано алгоритмічну розв’язність проблем наявності логічного наслідку для скінчених множин формул, проблем неспростовності та тотожної істинності для формул. In this paper we specify sequent calculi for free-quantifier functional logics and their variants with weak and strong equality. The introduced calculi formalize irrefutability, truth, falsity and strong logical consequence relations. For the proposed calculi we prove the soundness and completeness theorems. On the base of the completeness theorems we obtain an algorithmic solvability of problems of existence of logical consequence for finite sets of formulas, irrefutability problems and identically truth problems for formulas.