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

• Veröffentlicht in: Штучний інтелект
• Datum: 2016
• ISSN: 1561-5359
• Hauptverfasser: Шкільняк, С.С., Волковицький, Д.Б.
• Format: Artikel
• Sprache: Ukrainisch
• Veröffentlicht: Інститут проблем штучного інтелекту МОН України та НАН України 2016
• Schlagworte: Теорія та засоби обчислювального інтелекту
• Online Zugang: https://nasplib.isofts.kiev.ua/handle/123456789/132088
• Назва журналу: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Zitieren: Секвенційні числення логік безкванторно-функціональних рівнів / С.С. Шкільняк, Д.Б. Волковицький // Штучний інтелект. — 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.