Основні наукові результати дисертації отримані у формі прикладних досліджень:● розроблено онтологічно-орієнтований метод подання бази знань в середовищі асистента доведення теорем Coq, що сприяє формалізації нових та існуючих онтологій, а також уможливлює застосування логік вищих порядків як інструменту підтримки прийняття рішення в інтелектуальних системах; ● розроблено архітектуру та програмну реалізацію інтелектуальної системи для управління персональними та колективними базами знань, яка володіє властивостями версійності, розподіленості, автономності та забезпечує можливість надійного підтвердження авторства;● розроблено приклади формального доведення істинності описових знань, зокрема, для задач проектного управління в ІТ-підприємстві, узгодженості матеріалів в мас-медіа та моделей інфраструктурних мереж, що сприяло перевірці гіпотез в напівавтоматичному режимі; ● здійснено порівняльний аналіз моделей подання знань, описової логіки та формальних систем теорії типів, а також особливостей їх застосування для подання знань різної природи, зокрема, описових речень природньої мови, логічних, математичних теорій та виразів; ● здійснено системний аналіз понять «знання» та «істинність знання», і арґументовано використання конструктивної логіки з метою усунення проблем Ґетьє, які компрометують традиційні методи обґрунтування істинності знання.^UThe main results of the dissertation are obtained in the form of fundamental and applied research:• the method for ontologies representation in the environment of Coq proof assistant has been developed, which contributes to the formalization of new and existing ontologies and enables the application of higher-order logics as a reliable decision-support tool;• the architecture and software implementation of an intelligent system for personal and shared knowledge bases management have been created, which has the properties of being autonomous, distributed, supports versioning and ensures reliable authorship confirmation;• the examples of knowledge bases and formal reasoning over them have been provided, in particular for the domains of information systems, mass media, and infrastructure networks, which facilitate a semi-automatic procedure of hypotheses testing;• the comparative analysis of knowledge representation models, description logic, type theories, their characteristic features, and applications to the encoding of the knowledge of the various kinds, including natural language sentences, logical and mathematical expressions, has been conducted;• the system analysis of the concepts “knowledge”, “truth of knowledge” and the argument on constructive logic adoption for the sake of Gettier problems elimination, which compromise traditional methods of knowledge justification, have been presented.