Skip to content

Conformance Coverage

Summary for evaluators comparing OntoLogos to HermiT, ELK, and other reasoners. OntoLogos v0.5 ships EL classification, RL saturation, and growing HermiT ports.

HermiT porting strategy

Tests are cataloged in tests/hermit/manifest.toml and implemented in ontologos-conformance.

Tier CI HermiT checkout required Purpose
A Always (cargo test -p ontologos-conformance) No Inlined RL logic + small fixtures
B Always for pizza; wine optional No (vendored under benchmarks/data/hermit/) ClassificationTest taxonomy goldens

Run locally:

cargo test -p ontologos-conformance

Optional full HermiT tree: set ONTOLOGOS_HERMIT_ROOT or clone to HermiT/ for additional fixtures.

See tests/hermit/README.md for maintainer setup.

Tier A coverage (RL engine)

Representative ported cases (see manifest for full list):

HermiT test Engine Capability
testSubsumption2 RL Existential subsumption via property hierarchy
testSubsumption3 RL Equivalent properties + existentials
testSameAs RL sameAs propagates class assertions
testEquivalentClassInstances RL Equivalent classes share instance types
testReflexiveAndSameAs RL Reflexive properties + sameAs
testIndividualRetrievalBug RL Property assertion indexing
testIsFunctionalObject RL Functional characteristic on sub-properties

Tier B coverage (EL engine)

HermiT test Status Notes
ClassificationTest.testPizza CI Vendored pizza.xml + golden .txt
ClassificationTest.testWine Optional Skips when horned-owl cannot parse wine.xml

EL golden conformance

Pizza EL taxonomy is checked in CI via benchmarks/scripts/compare-elk.sh against committed benchmarks/data/pizza-el-golden.json. Regenerate baselines from ELK or whelk-rs when updating the EL engine.

Known gaps (v0.5)

Area Status
Full OWL DL Not shipped (2.0 target)
Complete OWL RL rule set Partial — see RL rules
Explanations Stub (v0.6)
Large DL corpora (GALEN, SNOMED) Optional stress tests only
Wine ClassificationTest Parser limitation on legacy RDF/XML

Benchmark corpora

Integration tests use Pizza (downloaded), Family (vendored), go-subset (vendored EL perf), and HermiT pizza fixtures. Manifest expected counts are mapper output, not Protégé logical axiom totals.

See benchmarks.md.