Overview
Reasoners: HermiT, ELK, Pellet, Konclude
Pick the reasoner that matches your profile and scale — not the one your tutorial used.
Why it matters
ELK is sub-second on million-class OWL EL ontologies; HermiT handles full DL but won't scale to those. Picking the wrong reasoner is the most common cause of 'OWL is too slow' complaints.
Going deeper
A practical pick-list, with the trigger that should send you to each reasoner:
| Reasoner | Pick when | Sweet spot | Watch-out |
|---|---|---|---|
| ELK | Your ontology is in OWL EL (taxonomy + existentials + intersections) | SNOMED CT-scale classification in seconds | No support for nominal-heavy ontologies or full DL features |
| HermiT | You need full OWL DL expressivity at human-readable speeds | Research models, general OWL 2 DL | Doesn't scale past ~50k classes; ABox reasoning is expensive |
| Pellet (now Stardog ICV) | You need DL + SWRL + integration with a triple store | Enterprise OWL+rules with explanations | Open-source line is mostly archived; modern fork lives inside Stardog |
| Konclude | Hardest DL problems, benchmark winner | Heavy DL benchmarks, optimisation showcases | Java + C++ stack, more setup overhead |
| JFact / FaCT++ | You want the classical tableau experience | Teaching, legacy tooling | Slower than ELK on EL; slower than HermiT on full DL |
Rule of thumb: start in ELK if your ontology is EL-compatible (you can check this with Protégé's OWL 2 Profile Validator). Promote to HermiT only when you discover an EL-illegal axiom you cannot remove. Reach for Stardog/Pellet when you also need SWRL rules or live querying with reasoning enabled.