open-ontologies

<!-- mcp-name: io.github.fabio-rovai/open-ontologies --> <p align="center"> <img src="docs/assets/logo.png" alt="Open Ontologies" width="170"> </p> <h1 align="center">Open Ontologies</h1> <p align="center"> <strong>Plan a change to a production ontology. See every consequence before you apply it.<br> Then give the reviewer a proof that they can check without trust in you.</strong><br> Open Ontologies is written in Rust. It ships as one binary. </p> <p align="center"> <a href="https://tesseractsemantics.com"><strong>tesseractsemantics.com</strong></a> </p> <p align="center"> <a href="https://tesseractsemantics.com"><img src="https://img.shields.io/badge/Tesseract%20Semantics-tesseractsemantics.com-111827?style=for-the-badge" alt="Tesseract Semantics"></a> <a href="https://github.com/fabio-rovai/open-ontologies/stargazers"><img src="https://img.shields.io/github/stars/fabio-rovai/open-ontologies?style=for-the-badge&logo=github&color=0b5fff" alt="Stars"></a> <a href="LICENSE"><img src="https://img.shields.io/badge/License-MIT-blue.svg?style=for-the-badge" alt="MIT"></a> <a href="https://github.com/fabio-rovai/open-ontologies/pkgs/container/open-ontologies"><img src="https://img.shields.io/badge/GHCR-pull%20the%20image-2496ED?style=for-the-badge&logo=docker&logoColor=white" alt="GHCR"></a> <a href="https://github.com/sponsors/fabio-rovai"><img src="https://img.shields.io/github/sponsors/fabio-rovai?style=for-the-badge&label=Sponsor&logo=GitHub%20Sponsors" alt="Sponsors"></a> </p> <p align="center"> <a href="https://www.star-history.com/fabio-rovai/open-ontologies"> <picture> <source media="(prefers-color-scheme: dark)" srcset="https://api.star-history.com/badge?repo=fabio-rovai/open-ontologies&type=trending&theme=dark"> <source media="(prefers-color-scheme: light)" srcset="https://api.star-history.com/badge?repo=fabio-rovai/open-ontologies&type=trending"> <img alt="GitHub Trending Repository of the Day" src="https://api.star-history.com/badge?repo=fabio-rovai/open-ontologies&type=trending"> </picture> </a> </p> <p align="center"> <strong>English</strong> · <a href="README.zh-CN.md">简体中文</a> </p> <p align="center"> <a href="https://open-ontologies-try.vercel.app/?sample=epc-sample.csv&auto=1"><img src="https://img.shields.io/badge/%E2%96%B6%20TRY%20IT%20IN%20THE%20BROWSER-e11d48?style=for-the-badge&labelColor=e11d48&color=e11d48" alt="Try it in the browser" height="44"></a> </p> <p align="center"> _{Put in one spreadsheet. Get one ontology, with the evidence for each line. Then change one cell, and see the shape find the error. The page runs the released binary.} </p> <p align="center"> <a href="https://tesseractsemantics.com"><b>Look for enterprise support? tesseractsemantics.com</b></a><br> _{The engine is MIT, and it stays MIT. The platform is the hosted version of the engine.} </p>

---

<p align="center"> <a href="docs/assets/knowledge-graph.svg"><img src="https://raw.githubusercontent.com/fabio-rovai/open-ontologies/main/docs/assets/knowledge-graph.webp" alt="A hand-drawn animation of ies-core.ttl. A person asserts the grey edges. The engine derives the green edges, and Lean 4 checks the one certificate that holds them. Four provers read the clauses and give opinions. A forged red line is refused, and a question the file cannot be asked comes back unasked." width="100%"></a> </p> <p align="center"> _{<b>426 asserted, 259 certified, 1 rejected.</b> The engine derived the green edges. A Lean 4 checker then <i>proved</i> them. One certificate holds all 259, and one run of the checker accepts it. The red edge is a forged line. The same checker refused that line, gave exit 1, and named the rule. The run supplies each count. Nobody writes a count into the caption.} </p> <p align="center"> <img src="https://raw.githubusercontent.com/fabio-rovai/open-ontologies/main/docs/assets/hqdm-audit.svg" alt="HQDM as two shipped files side by side. Left, the RDFS rendering: 23 terms used as a class but never declared drawn as hollow red rings and 12 rdfs:range declarations naming a relation drawn as red edges. Right, the OWL rendering: 190 named classes this engine found satisfiable and 39 it found unsatisfiable drawn red, with a red ring on the 39 that HermiT calls unsatisfiable, the same 39." width="100%"> </p> <p align="center"> _{<b>The same machinery, on a file from a different group, two times. HQDM ships as two files.</b> <code>hqdmTop/hqdmFramework</code> publishes an RDFS file. MagmaCore keeps a copy of that file, byte for byte. <code>gchq/HQDM</code> publishes an OWL file. The two files fail different checks. The RDFS file has no <code>owl:</code> term and no disjointness axiom. Thus <i>no named class in that file can be unsatisfiable</i>. But the file has <b>23</b> terms that it uses as a class and never declares. It has <b>12</b> <code>rdfs:range</code> declarations that name a relation and not a class. It also has <b>13</b> pairs of names that differ by one final underscore. Three of those pairs have the same domain and the same range. The OWL file passes all three checks, and the OWL file is not coherent. The tableaux of this engine finds <b>190</b> of its named classes satisfiable. The tableaux finds <b>39</b> unsatisfiable. HermiT calls the same <b>39</b> unsatisfiable, and HermiT is an opinion in the vocabulary of this repository. This figure proves nothing, and the figure does not claim a proof. A test computes each count again, and the test also computes that intersection. For the source and the method, read <a href="docs/assets/hqdm/PROVENANCE.md"><code>docs/assets/hqdm/PROVENANCE.md</code></a>.} </p>

One triple. Nothing added, nothing removed, blast radius zero. 901 consequences that were not there before.

$ printf 'load base.ttl\nplan proposed.ttl\n' | open-ontologies batch -
#   the whole change:  ex:hasParent rdfs:domain ex:Person

added_classes         0
removed_classes       0
blast_radius          0 triples affected
risk_score            low
                      ────────────────────────────────────────────
conservativity        not_conservative_under_rule_table
new consequences      901          rule table owl-rl, in 0.04s

Each number from a shape diff tells you that this change is safe. But the change gave a new type to each individual that the property already had. The tool closes this gap. A text diff cannot show you the gap. The change is one correct line, and the text diff is one line long.

Then give the reviewer the proof. The run writes a certificate. A different person re-verifies months later. That person needs no instance of this software and no network. The command is oo-cert asserted.tsv derivations.tsv. The exit code is 0, and the theorem OOCert.certificate_sound covers the result.

The checker also refuses a forged proof. Write a false conclusion into the derivation file. The same checker exits 1 and names the rule that does not hold. This is the red edge in the figure above. This refusal, and not the headline, is the part that survives examination.

This is not an ontology editor. Use Protégé to draw class hierarchies. You run Open Ontologies on the change, before the change goes to production.

The tool is like Terraform, and this is on purpose. But the plan is semantic, not syntactic. A text diff is git diff, and you have git diff already.

You do not need a JVM. You do not need Protégé. The engine speaks MCP to Claude, to Cursor, and to other clients of that protocol.

See the engine at work

<p align="center"> <img src="https://raw.githubusercontent.com/fabio-rovai/open-ontologies/main/docs/assets/demo-certify.svg" alt="A terminal runs the Lean certificate checker while a supplier graph lights up beside it: three asserted edges in grey, three derived edges in green that the checker accepts, then one conclusion forged and the same checker refusing it in red" width="940"> </p>

Three triples go in, and three triples come out. A person asserted only that ex:Northwind is in a sanctioned jurisdiction. The engine derived the need for enhanced due diligence. A different person can check that derivation. That person does not have to trust you, or this engine, or the model that wrote the ontology.

Watch the last seconds. Somebody forges one conclusion, and leaves the two premises exactly as they were. The same checker refuses the conclusion and names the rule. oo-horn printed each line in that terminal for the fixtures in tests/fixtures/horn/supplier/. A test runs the checker again. The test fails if the figure and the checker do not agree.

With a proof, and without a proof

| | An ordinary reasoner | Open Ontologies | | --- | --- | --- | | The answer | Northwind needs enhanced due diligence | the same answer | | Why the answer holds | "the reasoner says so" | a certificate that names each rule and each premise | | Who can check the answer | a second implementation can agree, and some reasoners give an explanation. No verified checker accepts either one | anybody, with a checker that shares no code with the engine | | If the engine has a defect | a second implementation can disagree. Then you know only that one of the two is wrong | the checker refuses the answer, exit 1 | | If a person edits the output | you cannot find the edit | the checker refuses it, and names the line and the rule | | If a rule was yours, not the standard's | the report is the same | a different verdict word, and a test holds that word | | What an auditor receives | a screenshot | a file that the auditor can check again | | Guarantee on an unsatisfiability answer | asserted | none, and the tool says so |

If the tool measures a property, the tool says measured. If a prover gives an opinion, that opinion never takes the vocabulary of the checker. Read what the tool proves, and what it does not prove.

What the tool does

| Capability | What you get | | --- | --- | | Reason over OWL and RDFS | Materialised inferences and a derivation certificate that a proved checker accepts | | Use your own rules | SWRL, RIF Core or a Horn table, evaluated, with a verdict word that says the rules were yours | | Validate against SHACL | A report from an evaluator with a measurement against the W3C suite, not an assertion of success | | Ask if something is satisfiable | A finite model, replayed and checked, and not only a yes | | Ask if something is inconsistent | A refutation, if one is certifiable. If not, an honest opinion from the engine | | Retrieve a slice for RAG | Entailment preservation for each claim, because 99% coverage can still lose the one triple that mattered | | Change an ontology in production | Plan, blast radius, risk score, locked IRIs, apply, monitor, drift, rollback | | Load real data | CSV, JSON, XML, YAML, XLSX, Parquet, PostgreSQL and DuckDB into RDF | | Give the problem to a prover | TPTP, CLIF, SMT-LIB and LADR from one translation. The tool names and counts what it cannot export | | Work from an assistant | An MCP server, so Claude or Cursor operates all of it in conversation |

Run the checker yourself

The repository holds the three files. The output shows only the important fields.

$ cd lean && lake build            # builds the checkers, core Lean 4, no Mathlib
$ F=../tests/fixtures/horn

$ lake exe oo-horn check $F/builtin_rules.tsv $F/asserted.tsv $F/good.tsv
{"ok":true,"verdict":"entailed","theorem":"OOCert.entails_of_builtin_horn",
 "means":"every conclusion is true in every model of the asserted graph"}

$ lake exe oo-horn check $F/builtin_rules.tsv $F/asserted.tsv $F/bad_conclusion.tsv
{"ok":false}                        # one IRI in the conclusion changed. exit 1.

$ lake exe oo-horn check $F/user_rules.tsv $F/asserted.tsv $F/good.tsv
{"ok":true,"verdict":"entaile