GitHub - Trivyn/growl: OWL RL Reasoner written in SLOP

An OWL 2 RL reasoner with Z3-verified inference rules.

Overview

Growl implements the OWL 2 RL profile inference rules with Z3-verified contracts on every inference function. Written in SLOP, it compiles to efficient C code while using SMT solving to prove properties about the inference logic.

Growl is being developed as the reasoning engine for Trivyn, a knowledge graph platform.

Features

• Z3-Verified Contracts: Every inference function has machine-checked pre/postconditions; soundness properties prove each output triple is justified by a delta/graph premise (see Verification for scope)
• OWL 2 RL Compliant: Implements W3C specification tables 4-9
• Parallel Execution: Fork-join parallel semi-naive evaluation
• Inconsistency Detection: Reports violations with witness triples

Rule Coverage

76 of 78 OWL 2 RL rules implemented (97% coverage). See detailed coverage table below.

API

;; Run reasoning with default configuration
(reason arena graph) -> ReasonerResult

;; Run with custom configuration
(reason-with-config arena graph config) -> ReasonerResult

;; Quick consistency check
(is-consistent arena graph) -> Bool

;; Query results
(get-types arena graph individual) -> (List Term)
(get-same-as arena graph individual) -> (List Term)

;; Annotation filtering (preprocessing)
(collect-annotation-properties arena graph) -> (Set Term)
(graph-to-indexed arena graph annot-set) -> IndexedGraph
(indexed-to-graph arena indexed-graph) -> Graph

Configuration

(record ReasonerConfig
  (worker-count Int)      ;; Number of parallel workers (default: 4)
  (channel-buffer Int)    ;; Message buffer size (default: 256)
  (max-iterations Int)    ;; Iteration limit (default: 1000)
  (verbose Bool)          ;; Print per-iteration timing (default: true)
  (fast Bool)             ;; Skip schema rules & checks (default: false)
  (complete Bool)         ;; Enable cls-thing & prp-ap (default: false)
  (enrich Bool)           ;; Property/subclass enrichment only (default: false)
  (validate Bool)         ;; Enable TBox validation mode (default: false)
  (validate-ns String))   ;; Only validate entities with this IRI prefix (default: "")

CLI Usage

growl [options] <file.ttl>

Options:
  -h, --help       Show help message
  -q, --quiet      Only print failures and inconsistencies
  -f, --fast       Skip schema rules and consistency checks
  -c, --complete   Enable cls-thing and prp-ap for spec completeness
  -e, --enrich    Property/subclass enrichment (skip sameAs, class exprs, schema)
  --validate       Check TBox satisfiability via synthetic instance injection
  --validate-ns NS Only validate entities with IRIs starting with NS
  -b, --background FILE  Load background ontology (e.g. TLO) for reasoning context
  -o, --emit FILE  Write materialized graph to TTL file
  -V, --version    Show version information

Complete Mode

The --complete flag enables axiom rules that are skipped by default for performance:

• cls-thing: Asserts owl:Thing rdf:type owl:Class
• cls-nothing1: Asserts owl:Nothing rdf:type owl:Class
• prp-ap: Asserts standard annotation properties (rdfs:label, rdfs:comment, etc.) as owl:AnnotationProperty
• dt-type2: Asserts literal rdf:type datatype for every typed literal with a supported datatype

These rules are spec-correct but produce triples with zero practical inference value. Use --complete for conformance testing against other reasoners like owlrl.

Enrich Mode

The --enrich flag materializes a targeted subset of rules — property characteristics and subclass/subproperty propagation — while skipping sameAs generators, class expressions, and schema materialization. This is useful for practical ontology enrichment without the overhead and triple explosion of full OWL reasoning.

Rules that run in enrich mode:

Rules skipped in enrich mode:

• sameAs generators: prp-fp, prp-ifp, prp-key (these produce owl:sameAs triples which can cause combinatorial explosion)
• All eq-* rules: No sameAs symmetry, transitivity, or replacement
• All cls-* rules: No class expression reasoning (intersectionOf, unionOf, someValuesFrom, hasValue, cardinality, etc.)
• All scm-* rules: No schema materialization (subClassOf/subPropertyOf closure, domain/range propagation through hierarchies)
• Datatype rules: dt-type1, dt-type2, dt-not-type

Enrich mode is a good fit when your ontology already has explicit subClassOf/subPropertyOf chains (most published ontologies do) and you want fast type propagation without the quadratic blowup from sameAs or class expression reasoning.

# Enrich an ontology with property/subclass inferences
growl --enrich ontology.ttl

# Enrich and emit the materialized graph
growl --enrich --emit enriched.ttl ontology.ttl

Validate Mode

The --validate flag enables TBox validation, which checks whether the class and property declarations in an ontology are satisfiable. Growl injects a synthetic blank node instance for each declared class and property, runs reasoning to fixpoint, then scans for inconsistencies triggered by these synthetic individuals.

The following check rules detect unsatisfiable entities: cls-nothing2, cax-dw, cax-adc, cls-com, prp-asyp, prp-pdw. Validate mode reports all unsatisfiable entities, not just the first.

Use --validate-ns to scope validation to a specific namespace. This is important when reasoning over a domain ontology that imports a large top-level ontology (TLO) — without namespace filtering, the TLO's classes would also be validated, which is usually not what you want.

Use --background to load a background ontology that provides reasoning context (e.g. class hierarchy, property declarations) without being validated itself. Background triples participate in inference but are not targets for synthetic instance injection.

Note: --validate overrides --fast, since schema materialization is required for validation to work correctly.

# Validate all classes/properties in an ontology
growl --validate ontology.ttl

# Validate only entities in a specific namespace
growl --validate --validate-ns "https://example.org/" ontology.ttl

# Validate a domain ontology against a background TLO
growl --validate --validate-ns "https://example.org/" --background tlo.ttl domain.ttl

Fast Mode

The --fast flag skips schema vocabulary rules (scm-*), datatype rules (dt-type1, dt-not-type), equality-difference checks (eq-diff1/2/3), eq-ref, and cardinality rules (cls-maxc1/2, cls-maxqc1-4). Consistency checks (cax-dw, cax-adc, prp-asyp, prp-irp, prp-pdw, prp-adp, prp-npa1/2, cls-nothing2, cls-com) still run in fast mode, matching the coverage of reasoners like reasonable. Most published ontologies already include explicit subClassOf/subPropertyOf chains, making schema closure unnecessary for practical use.

Annotation Filtering

Growl provides annotation filtering as a preprocessing step. Annotation properties have no semantic effect under OWL 2 Direct Semantics — they carry human-readable metadata (labels, comments, descriptions) that cannot trigger any inference rule. Removing them reduces the input graph size without affecting reasoning results.

The following properties are filtered by default:

• OWL/RDFS (9): rdfs:label, rdfs:comment, rdfs:seeAlso, rdfs:isDefinedBy, owl:deprecated, owl:versionInfo, owl:priorVersion, owl:backwardCompatibleWith, owl:incompatibleWith
• SKOS (10): skos:prefLabel, skos:altLabel, skos:hiddenLabel, skos:definition, skos:note, skos:scopeNote, skos:example, skos:historyNote, skos:editorialNote, skos:changeNote
• Dublin Core (8): dc:title, dc:creator, dc:subject, dc:description, dcterms:title, dcterms:creator, dcterms:description, dcterms:abstract

Additionally, any property declared as owl:AnnotationProperty in the input graph is filtered. This is significant for large ontologies — for example, CCO drops from ~13.6K to ~6K input triples.

Library Usage

;; Build annotation property set from parsed graph
(let ((annot-set (collect-annotation-properties arena g))
      (ig (graph-to-indexed arena g annot-set)))
  ;; Run reasoning on filtered graph
  (match (reason arena ig)
    ((reason-success s)
      ;; Convert back for serialization, re-adding annotations
      (let ((mut out-ig (. s graph)))
        (for-each (t (. g triples))
          (when (set-has annot-set (. t predicate))
            (set! out-ig (indexed-graph-add arena out-ig t))))
        (indexed-to-graph arena out-ig)))
    ((reason-inconsistent _) ...)))

CLI

The CLI applies annotation filtering automatically. When --emit is used, filtered annotation triples are re-added to the output so no data is lost in the materialized graph.

Building

slop build src/growl.slop

Building from C

Pre-transpiled C sources are included in csrc/, so you can build with just a C compiler — no SLOP toolchain required.

make            # build cli → build/growl
make lib        # build static library → build/libgrowl.a
make release    # optimized build (-O3, NDEBUG)
make test         # build and run tests
make benchmark    # run benchmarks
make conformance  # per-rule + multi-rule interaction tests (92 tests)
make reference    # accuracy tests against OWL-RL reference reasoner

Rust Bindings

Safe Rust bindings are available in the rust/ directory. See rust/README.md for usage instructions.

Benchmarks

Compared against OWL-RL (Python reference implementation, used as ground truth) and Reasonable (Rust) on 5 real-world ontologies. Growl filters annotation triples before reasoning (see Annotation Filtering), so its effective input is smaller — the "Input" column shows the raw triple count that OWL-RL and Reasonable see.

Performance

Accuracy (inferred triples vs OWL-RL reference)

Modes: --complete enables all spec rules (cls-thing, prp-ap, dt-type2) for closest OWL-RL parity. Default Growl skips those practically inert rules. --enrich runs only property/subclass propagation and consistency checks (no sameAs, class expressions, or schema materialization). --fast targets the same rule coverage as Reasonable (skips schema rules, datatypes, eq-ref, cardinality), making Growl --fast vs Reasonable an apples-to-apples comparison.

Verification

slop verify              # verify all files in [verify].sources
slop verify -v           # verbose — shows per-function results

Growl uses slop verify, which encodes contracts into Z3 SMT formulas and proves them with weakest-precondition calculus. 104 function-level contracts are verified across the codebase.

What is proven:

• Soundness (@property soundness): For every output triple, there exists a delta triple justifying it — proving the reasoner never fabricates conclusions from nothing. Covers 56 of 77 inference functions, including all high-value rules (cax-sco, prp-dom/rng, eq-ref/sym, cls-hv1/hv2, etc.).
• Completeness (@property completeness): For certain rules (eq-sym/trans, prp-symp, scm-cls, scm-eqc1/eqc2, scm-eqc-mutual, scm-eqp1/eqp2, scm-eqp-mutual, scm-op, scm-dp), every applicable delta triple produces the expected output — proving the reasoner doesn't miss inferences. 12 functions.
• Novelty (@property novelty): Every output triple is new — not already present in the graph. Proves the rule engine never wastes work emitting redundant inferences. Covers cls-maxc2, cls-maxqc3, cls-maxqc4, and transitive-closure (4 functions).
• Postconditions (@post): Predicate constraints (e.g. all outputs have rdf:type as predicate), witness counts on inconsistency reports, iteration numbering, and result bounds.
• Preconditions (@pre): Graph size non-negativity, valid input constraints.

What is not proven:

• Soundness for deeply nested callback functions (cls-maxc2/maxqc3/4) that only query the full graph — these don't iterate delta, so the standard delta-sourcing property doesn't apply. They have @property novelty and @post predicate checks instead.
• Full join semantics — soundness contracts prove delta-sourcing (every output links to a delta triple) but don't fully encode the multi-way join conditions of rules like cls-int1 (which requires checking all intersection components).
• Termination of the fixed-point loop is not proven (semi-naive evaluation over finite graphs terminates in practice but isn't formally verified).
• Memory safety of the generated C code is not verified (relies on arena allocation patterns).

OWL 2 RL Rule Coverage

Detailed per-rule coverage against the W3C OWL 2 RL specification.

Table 4 — Equality (9/9)

Table 5 — Property Axioms (20/20)

Table 6 — Class Expressions (19/19)

Table 7 — Class Axioms (5/5)

Table 8 — Datatypes (3/5)

Table 9 — Schema Vocabulary (20/20)

License

Apache License 2.0 - see LICENSE for details.