Knowledge Representation and Formal Reasoning in Ontologies with Coq

The paper describes a modern type-theoretical approach to the knowledge representation and formal reasoning in ontologies. The current state and limitations of the adopted technology for reasoning in ontologies as well as the advantages of the proposed approach are highlighted. Curry-Howard correspondence and its role in the establishment of computational reasoning are emphasized. The main part is dedicated towards the representation of ontology elements in Coq proof assistant and the execution of a semi-automated reasoning over them.