v0.1.0

The first release. HOWL classifies OWL ontologies: the complete subsumption hierarchy, every
unsatisfiable class, and whether the ontology is coherent, including the subsumptions that follow
from defined classes, which OWL 2 RL materialization cannot see.

What's in it

• Two profiles, both polynomial.
  • el (the default): ELH⊥R+ with domains, ranges, ABox assertions, and ¬ in a superclass,
    domain or range.
  • el++: the OWL 2 EL object fragment, adding nominals, hasValue, hasSelf, reflexive roles,
    individual equality and inequality, and negative assertions.
  • auto picks the cheapest profile that covers the ontology.
• The howl CLI.
  • howl validate exits 0 (coherent), 1 (incoherent), 2 (inconclusive — not a pass) or 3 (error).
  • Flags: -I for attested imports, --profile, --strict, --report (a canonical, hashable
    report), --workers, --max-iterations, --timings and --version.
• A C library.
  • libhowl.a with include/howl.h. The API is written in SLOP and its header is generated by
    slop.
  • Inputs and runs are opaque handles. Turtle and triple input, attested imports and cancellation
    are supported. See examples/c/classify.c.
• A Rust crate in rust/, a safe wrapper over the C API. It is not on crates.io yet.

What it guarantees

• Nothing is silently dropped. Every axiom HOWL does not reason over is listed as an omission,
  and any omission makes an otherwise clean run inconclusive.
• A finding beats incomplete coverage. An incoherence found under partial coverage is still
  reported as incoherent.
• Reports are input-determined. For a given round cap, the canonical report is byte-identical
  at every worker count, and it never contains a timing, path or worker count.

Evidence

• Differential testing:
  • every fixture against HermiT, and against ELK where ELK is probed capable of the construct.
    The one exception is owl:Thing ⊑ owl:Nothing, which HermiT cannot load; it is checked against
    ELK alone;
  • the in-profile part of RO, OBI, the Gene Ontology and EL-GALEN against its routed oracle, over
    every pair of named classes.
• Conformance: the W3C OWL 2 and ELK conformance suites, wherever HOWL reasons completely.
• Fuzzing: 400 generated ontologies with ABoxes per profile, matched against HermiT.
• Performance: el classifies within 5× of ELK, the SPEC §12 target. On an Apple M3 Ultra,
  the Gene Ontology runs at 0.84× ELK's time and EL-GALEN at 2.9×. el++ has no target. It runs
  at 0.95× and 5.25×.
• Contracts: 89 functions carry Z3-checked contracts, among them the profile selection, the
  verdict's safety property and each el++ rule's faithfulness.

Known limitations

• Unbuilt profiles. horn-sriq and sriq are not built; asking for one exits 3.
• Omitted constructs. HasKey, datatypes and data properties, and constructs outside OWL 2 EL
  (unions, universal restrictions, cardinalities, inverse properties) are reported as omissions.
• No howl classify yet. howl classify (--emit, --reduce) is refused until a later
  release.
• MOOSE port amendments. The TBoxReasoner port amendments (SPEC §8.5) are on the consumer
  side and not delivered here.
• Contract checking. make verify needs a slop toolchain from before 0.4.0 until
  slop-lang/slop#325 is fixed; the committed C is generated by slop 0.4.0 and slop-rdf 0.5.0.
• Prebuilt binaries are for linux-x86_64 and macos-arm64 only. Elsewhere, make builds from the
  committed C with any C compiler.