fabio-rovai/open-ontologies

Plan a change to a production ontology. See every consequence before you apply it.
Then give the reviewer a proof that they can check without trust in you.
Open Ontologies is written in Rust. It ships as one binary.
tesseractsemantics.com
English · 简体中文
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.
Look for enterprise support? tesseractsemantics.com
The engine is MIT, and it stays MIT. The platform is the hosted version of the engine.
---
426 asserted, 259 certified, 1 rejected. The engine derived the green edges. A Lean 4
checker then proved 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.
The same machinery, on a file from a different group, two times. HQDM ships as two files.
hqdmTop/hqdmFramework publishes an RDFS file. MagmaCore keeps a copy of that file, byte
for byte. gchq/HQDM publishes an OWL file. The two files fail different checks. The RDFS
file has no owl: term and no disjointness axiom. Thus no named class in that file can be
unsatisfiable . But the file has 23 terms that it uses as a class and never declares. It has
12 rdfs:range declarations that name a relation and not a class. It also has 13
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 190 of its named classes satisfiable. The tableaux finds 39 unsatisfiable.
HermiT calls the same 39 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
docs/assets/hqdm/PROVENANCE.md .
One triple. Nothing added, nothing removed, blast radius zero. 901 consequences that were not there before.
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
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 |