Supporting the 2025 ontology summit: OWL2 ontology. Towards a formal theory
alex.shkotin
We have found that the system of formal definitions in GENO is the beginning of an axiomatic theory in which some terms will be primary, and the rest will receive formal definitions based on them.
Of course, this is a lot of work and a start has been made.
Let us describe a regular way in which the construction of a formal theory can be continued.
1) A corpus of documents (books, articles, reports, etc.) is recorded, which contain theoretical knowledge about a given subject area.
2) A dictionary of terms of the subject area is compiled in the form of an ontology. It records all available definitions of terms with an indication of the source in the corpus of documents.
3) Definitions are verified from the point of view of logical correctness, since specialists in the subject area often use rather free formulations, including those containing unnecessary information. For example, they contain examples of entities falling under a given concept.
It is quite possible that the logical definition will not be accepted by experts as the main one, i.e. they will not switch to it. But what experts must confirm is that their definition and the logical one are equivalent. It often happens that one person gives a definition Def1 and stands for each letter in it, and another - Def2, and stands his ground. And we have to prove the equivalence theorem
∀x Def1(x)≡Def2(x).
4) Logical definitions can already be formalized by constructing a hierarchy of definitions of terms and identifying primary classes, binary relations and attributes.
5) As soon as the axioms connecting them are found for the primary terms, we will obtain a formal axiomatic theory.