Ontologies that reason

The concepts do the reasoning

Description Logic is the mathematics underneath OWL and the semantic web. You declare concepts (classes) and roles (binary relations), compose them into concept expressions, and a reasoner decides — by construction, not by lookup — whether a class is consistent, whether one class is contained in another (subsumption), and whether an individual belongs to a class. Axioma implements the ALC fragment on a sound tableau (reasoner/sat.go) with proper disjunction-branching, so the answers are decidable and correct — not the pattern-matching approximation naive engines ship. The operators below run either as glyphs (⊓ ⊔ ¬ ⊑ ≡) or as ASCII backtick digraphs (`sqcap etc.) — no special keyboard required.

Concept algebra — ⊓, ⊔, ¬ build first-class expressions

Intersection ⊓, union ⊔, and complement ¬ combine declared concepts into a ConceptExpr value you can name, pass around, and query. @expr reports its type; the same value flows into satisfiable, ⊑, and is below.

Satisfiability — the tautology naive engines get wrong

A class is satisfiable if some model can populate it. Student ⊓ ¬Student is a contradiction — false. But Student ⊔ ¬Student is the law of excluded middle, so it must be true — and a reasoner that treats ⊔ as ⊓ (adding both disjuncts to one node) wrongly reports it unsatisfiable. Axioma's tableau branches on disjunction, so it decides both correctly.

Subsumption — containment decided over the TBox

Declaring Dog extends Animal is a told subsumption; Dog ⊑ Animal then reads in the textbook direction — the left is the more specific concept. The English word subsumes reads the converse. Compound sides like (Dog ⊓ Robot) ⊑ Dog aren't asserted anywhere — the tableau derives them.

Defined concepts — a role restriction plus membership

concept Parent ≡ Person ⊓ (∃hasChild: Person) is a necessary-and-sufficient definition (a general concept inclusion): a role restriction ∃hasChild: Person says "has some child that is a Person." Subsumption follows from the definition intensionally; and closed-world is classifies actual individuals — alice, who has a child, qualifies; childless bob does not.

Partitions & ⊤ / ⊥ — disjointness, covering, and the universe

A partition compiles to real TBox axioms: the members become pairwise disjoint and jointly cover the parent — so no cat is a dog, and every animal is exactly one of cat/dog/fish. Thing (⊤) and Nothing (⊥) are seeded system concepts (OWL's owl:Thing / owl:Nothing): ⊤ subsumes everything, and ⊥ is unsatisfiable by definition.