Open Ontologies is an ontology engine, shipped as a single Rust binary with an MCP server, that reasons over OWL and RDFS ontologies and writes a derivation certificate for each answer. A separate checker written in core Lean 4, which shares no code with the engine, re-verifies the certificate offline: it re-derives every conclusion from its premises under the named rule, accepts a valid certificate with a soundness theorem, and refuses a forged or edited line with exit code 1, naming the line and the rule. Anyone holding the certificate files (a reviewer in CI, an auditor months later, or another agent receiving a claim) can run the check without trusting the engine or the model that wrote the ontology.
The engine is aimed at changes to ontologies in production rather than at authoring them, and it states that it is not an ontology editor. Its workflow resembles a Terraform plan made semantic: plan a change, see added and removed classes, blast radius, a risk score, and the new consequences it entails, then apply it, watch for drift, certify what was derived, and roll back. A one-line change that a text diff shows as harmless can surface hundreds of new inferences in the plan.
Reasoning covers RDFS, OWL RL rules, a native OWL2-DL tableaux reasoner, and user-supplied SWRL, RIF Core, or Horn rules. When a rule came from you rather than the standard, the verdict word changes so the certificate records it as an assumption. Where the tool cannot certify an answer (for example an unsatisfiability result), it says so. Storage and SPARQL 1.1 run on Oxigraph, in memory by default, with no JVM required.
Claude, Claude Code, Cursor, and other MCP clients operate the engine in conversation. The repository also includes a pure-Python engine checked by the same Lean binaries, a marketplace of 33 standard ontologies, clinical crosswalks, semantic embeddings, and a desktop Studio with an ontology tree, an AI chat panel, and an inspector.
Features
- Derivation certificates: each reasoning run writes a certificate that names every rule and premise, checked by a Lean 4 checker with a soundness theorem
- Forgery detection: the checker refuses an edited or forged conclusion and reports the line number, the rule, and the premises
- Change planning: plan, apply, monitor, drift, and rollback for production ontologies, with blast radius, risk score, locked IRIs, and new entailed consequences
- Custom rules: SWRL, RIF Core, or Horn tables, flagged with a distinct verdict when the rules are yours
- SHACL validation: reports from an evaluator measured against the W3C test suite
- Satisfiability checks: returns a finite model that is replayed and checked, or a refutation when one is certifiable
- RAG slices: retrieves an ontology slice and checks that each claim's entailments are preserved
- Data loading: CSV, JSON, XML, YAML, XLSX, Parquet, PostgreSQL, and DuckDB converted into RDF
- Prover export: translates to TPTP, CLIF, SMT-LIB, and LADR, and lists what it cannot export
- MCP server: exposes the ontology tools to Claude, Cursor, Windsurf, Zed, and VS Code
