Essence of ontology reasoning
Description Logic, Tboxes, Aboxes, and the Tableaux algorithm for consistency checking. The formalism behind knowledge bases like SNOMED and OWL.
Ontologies are used across healthcare and the semantic web to define shared vocabularies and structured knowledge. SNOMED encodes clinical terminology; OWL underpins much of the web's linked data infrastructure. The formal backbone is Description Logic, which extends propositional logic with operators for classes, instances, and properties, split into a Tbox (facts about classes) and an Abox (facts about individual instances).
The article covers the ALC description logic, how to read Tbox and Abox axioms, and how Tableaux calculus checks whether a knowledge base is consistent by applying five expansion rules and looking for contradictions. A worked example walks through the full algorithm step by step. Published on Medium, October 2020.