Lenko V. Methods and tools for personal knowledge management in intelligent systems

The 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.