A sound disjunctive context reasoner for SROIQ / OWL 2 DL, with machine-checked soundness in Lean 4 and per-run verified certificate checking. - View it on GitHub