The reasoning boundary La frontière de raisonnement

Publishing an ontology creates obligations a file does not state. An OWL axiom entails consequences, and a triple store does not compute them. This page says exactly which consequences the bra0 ontologies carry, which tool establishes each kind of fact, and what the toolchain does not do — so that nobody reads a green check as an answer to a question it never asked. Publier une ontologie crée des obligations qu'aucun fichier n'énonce. Un axiome OWL entraîne des conséquences, et un magasin de triplets ne les calcule pas. Cette page dit précisément quelles conséquences portent les ontologies bra0, quel outil établit chaque sorte de fait, et ce que la chaîne d'outils ne fait pas — pour que personne ne lise un vert comme la réponse à une question qu'il n'a jamais posée.

An entailment is not a suggestion Un entailment n'est pas une suggestion

Three ordinary axioms, each in a different file, none of them unusual. A property declares its domain; that domain is a subclass of something; that something is grounded in an upper ontology. Assert one triple and three more follow: Trois axiomes ordinaires, chacun dans un fichier différent, aucun inhabituel. Une propriété déclare son domaine ; ce domaine est sous-classe de quelque chose ; ce quelque chose est ancré dans une ontologie de haut niveau. Assertez un triplet, trois autres suivent :

• asserted<x> edgy:has <some capability>
• entailed<x> a edgy:Organization  — rdfs:domain
• entailed<x> a edgy:People  — rdfs:subClassOf
• entailed<x> a obo:BFO_0000004  — BFO grounding

No file states the last three. A SPARQL query asking whether <x> is an organisation answers false — and that false measures the engine, not the graph. This is not a defect in SPARQL: a query answers about assertions, and asking it about membership is a category error that produces a plausible wrong answer rather than an error message. The failure direction reads as success, which is why it must be written down. Aucun fichier n'énonce les trois derniers. Une requête SPARQL demandant si <x> est une organisation répond false — et ce false mesure le moteur, pas le graphe. Ce n'est pas un défaut de SPARQL : une requête répond sur des assertions, et lui poser une question d'appartenance est une erreur de catégorie qui produit une réponse fausse plausible plutôt qu'un message d'erreur. L'échec se présente comme un succès, et c'est pourquoi il faut l'écrire.

Which logic the bra0 ontologies are in Dans quelle logique sont les ontologies bra0

Which consequences follow, and which engine can compute them, is decided by the constructors the ontologies actually use — not by the format they are written in. Measured over the live corpus, excluding archives, deprecations and raw upstream imports: Quelles conséquences suivent, et quel moteur peut les calculer, est décidé par les constructeurs que les ontologies emploient réellement — pas par le format dans lequel elles sont écrites. Mesuré sur le corpus vivant, hors archives, dépréciations et imports amont bruts :

Measured absent: every cardinality form, property chains, reflexivity, irreflexivity, asymmetry, role disjointness, keys, owl:sameAs, owl:differentFrom, owl:complementOf, owl:allValuesFrom. The live corpus has no transitive role at all. Mesurés absents : toute forme de cardinalité, les chaînes de rôles, la réflexivité, l'irréflexivité, l'asymétrie, la disjonction de rôles, les clés, owl:sameAs, owl:differentFrom, owl:complementOf, owl:allValuesFrom. Le corpus vivant n'a aucun rôle transitif.

That set of constructors names a description logic: ALCHOIF(D) for the live corpus. It is a strict sublogic of SROIQ(D), which is OWL 2 DL. Cet ensemble de constructeurs nomme une logique de description : ALCHOIF(D) pour le corpus vivant. C'est une sous-logique stricte de SROIQ(D), qui est OWL 2 DL.

Consequence: which OWL 2 profile applies Conséquence : quel profil OWL 2 s'applique

This matters practically rather than academically. A reasoner is complete only for its profile: routing an ontology to an engine whose profile it falls outside of is not merely slower or less thorough — the engine's guarantees do not apply to it. The profile verdict therefore comes before any question about an engine's rule coverage. Cela compte pratiquement, non académiquement. Un raisonneur n'est complet que pour son profil : router une ontologie vers un moteur dont elle sort n'est pas seulement plus lent ou moins minutieux — les garanties du moteur ne s'y appliquent pas. Le verdict de profil précède donc toute question sur la couverture de règles d'un moteur.

The division of labour Le partage du travail

Four questions a reader might expect an ontology to answer. Only one of them needs a reasoner, and saying which is how over-equipment is avoided. Quatre questions qu'un lecteur pourrait attendre d'une ontologie. Une seule exige un raisonneur, et le dire est la manière d'éviter le sur-équipement.

This is why bra0 carries its constraints in SHACL rather than encoding them as OWL axioms wherever both would work. A SHACL shape renders a report naming each violation, its focus node and its source shape; an OWL axiom renders an entailment that something must then compute. For a constraint you want to enforce, the report is the useful artefact. C'est pourquoi bra0 porte ses contraintes en SHACL plutôt que de les encoder en axiomes OWL partout où les deux marcheraient. Une forme SHACL rend un rapport nommant chaque violation, son nœud focal et sa forme source ; un axiome OWL rend un entailment qu'il faut ensuite calculer. Pour une contrainte qu'on veut faire respecter, le rapport est l'artefact utile.

What the toolchain does not do Ce que la chaîne d'outils ne fait pas

Stated plainly, because a reader who assumes otherwise will misread every green check: Dit franchement, parce qu'un lecteur qui suppose l'inverse mélira chaque vert :

• No entailment is computed by default. Queries answer about assertions. Where a question is about membership, the graph must be materialised first or the question must be routed to a reasoner. Aucun entailment n'est calculé par défaut. Les requêtes répondent sur des assertions. Quand une question porte sur l'appartenance, le graphe doit d'abord être matérialisé ou la question routée vers un raisonneur.
• Inconsistency is not detected by SPARQL materialisation. A rule set that propagates subclasses and domains derives no contradiction, however many rules it has. Only a consistency check does, and that is a reasoner's task. L'inconsistance n'est pas détectée par une matérialisation SPARQL. Un jeu de règles qui propage sous-classes et domaines ne dérive aucune contradiction, quel que soit son nombre de règles. Seule une vérification de consistance le fait, et c'est l'affaire d'un raisonneur.
• Materialising into the graph loses provenance unless derived triples go to a separate named graph. A derived triple written beside an asserted one is indistinguishable from it, and the next diff of the file shows an inference as authored content. Matérialiser dans le graphe perd la provenance si les triplets dérivés ne vont pas dans un graphe nommé distinct. Un triplet dérivé écrit à côté d'un asserté en est indiscernable, et le prochain diff du fichier montre une inférence comme du contenu rédigé.

A sound engine's negative is not a verdict Le négatif d'un moteur solide n'est pas un verdict

An engine can be sound without being complete, and almost every practical reasoner is. Soundness is a promise about what the engine says: everything it asserts is genuinely entailed. Completeness would be a promise about what it finds: nothing entailed escapes it. The second promise is the expensive one, and a reasoner that declines it is being honest rather than deficient. Un moteur peut être solide sans être complet, et presque tout raisonneur pratique l'est. La solidité est une promesse sur ce que le moteur affirme : tout ce qu'il énonce est réellement entailé. La complétude serait une promesse sur ce qu'il trouve : rien d'entailé ne lui échappe. La seconde promesse est la coûteuse, et un raisonneur qui la décline est honnête plutôt que déficient.

The consequence is asymmetric, and it decides how a gate may be armed. A consistency check returning false has found a contradiction, and soundness makes that finding trustworthy. The same check returning true has found nothing — which, absent completeness, says nothing about whether anything is there. One direction is evidence. The other is silence wearing the same word. La conséquence est asymétrique, et elle décide de la façon d'armer une barrière. Une vérification de consistance qui rend false a trouvé une contradiction, et la solidité rend cette trouvaille fiable. La même vérification qui rend true n'a rien trouvé — ce qui, sans complétude, ne dit rien sur ce qui s'y trouve. Un sens est une preuve. L'autre est un silence qui porte le même mot.

We measured this on ourselves rather than reasoning about it. The W3C OWL 2 test suite publishes premises it declares unsatisfiable; a reasoner's required answer is false, every time. Against that external oracle, on 2026-10-17: Nous l'avons mesuré sur nous plutôt que raisonné dessus. La suite de tests W3C OWL 2 publie des prémisses qu'elle déclare insatisfiables ; la réponse exigée d'un raisonneur est false, chaque fois. Face à cet oracle externe, le 2026-10-17 :

The first row and the second are the point. The controls we wrote ourselves passed; the oracle we did not write answered none of fifty-two. Three competing explanations were eliminated before this was published, because the first draft blamed the engine. The premises did load — the engine's own statistics report them absorbed, so this is not the empty-graph trap where nothing read is trivially consistent. The cases are in scope — the suite's manifest declares 127 of its 128 applicable under direct semantics, which refutes the convenient hypothesis that these were RDF-based tests a DL reasoner need not answer. And the engine did not flag a limit: every one of the thirty returned incomplete: false with nothing dropped. La première ligne et la deuxième sont le propos. Les contrôles que nous avons écrits nous-mêmes passent ; l'oracle que nous n'avons pas écrit n'en répond aucun sur cinquante-deux. Trois explications concurrentes ont été écartées avant publication, car le premier jet accusait le moteur. Les prémisses se sont chargées — les statistiques du moteur les rapportent absorbées, ce n'est donc pas le piège du graphe vide où ce qui n'est pas lu est trivialement consistant. Les cas sont dans le périmètre — le manifeste de la suite en déclare 127 sur 128 applicables en sémantique directe, ce qui réfute l'hypothèse commode de tests RDF-based auxquels un raisonneur DL n'aurait pas à répondre. Et le moteur n'a pas signalé de limite : chacun des trente a rendu incomplete: false, sans rien d'abandonné.

So the engine is exonerated and the defect is ours. Its documentation states the guarantee in exactly the right direction — positives may be missed, never falsely asserted — and an incomplete flag that counts dropped axioms was never a claim about what the calculus can reach. A field naming what an engine discarded does not bound what it cannot see. What was wrong was our routing table, which carried this engine as the canonical implementation for consistency with no verdict contract attached, so a gate could have been armed on the untrustworthy direction and passed a corpus carrying any of those thirty contradiction shapes. Le moteur est donc exonéré et le défaut est le nôtre. Sa documentation énonce la garantie exactement dans le bon sens — des positifs peuvent être manqués, jamais faussement affirmés — et un drapeau incomplete qui compte des axiomes abandonnés n'a jamais été une affirmation sur ce que le calcul atteint. Un champ qui nomme ce qu'un moteur a écarté ne borne pas ce qu'il ne voit pas. Ce qui était faux, c'est notre table de routage, qui portait ce moteur comme implémentation canonique de la consistance sans contrat de verdict, de sorte qu'une barrière aurait pu être armée dans le sens non fiable et laisser passer un corpus portant l'une de ces trente formes de contradiction.

• The arming rule. Where an engine guarantees soundness and not completeness, only its positive answer arms a gate. The negative declares a gap. La règle d'armement. Quand un moteur garantit la solidité et non la complétude, seule sa réponse positive arme une barrière. Le négatif déclare une lacune.
• Every engine row states its verdict contract as data, beside the engine, so no gate author has to rediscover the asymmetry. Chaque ligne de moteur énonce son contrat de verdict en donnée, à côté du moteur, pour qu'aucun auteur de barrière n'ait à redécouvrir l'asymétrie.
• Every call carries a time bound. The two unbounded invocations that met case 53 held a processor core each for three hours of CPU, in an active loop, and would not have stopped on their own. Chaque appel porte une borne de temps. Les deux invocations non bornées qui ont rencontré le cas 53 ont tenu un cœur de processeur chacune pendant trois heures de CPU, en boucle active, et ne se seraient pas arrêtées seules.
• Our own green is demoted by the same rule. “The corpus is consistent” now reads “no contradiction was found within the implemented fragment”. The three contradictions the engine did find that day remain evidence, because false is the trustworthy direction. Notre propre vert est rétrogradé par la même règle. « Le corpus est consistant » se lit désormais « aucune contradiction n'a été trouvée dans le fragment implémenté ». Les trois contradictions que le moteur a trouvées ce jour-là restent des preuves, car false est le sens fiable.

The families the fragment missed are worth naming, because they are where an ontology actually breaks in practice: contradictions at the instance level rather than between classes — negative property assertions, mutually distinct individuals, disjoint class and property sets, zero-maximum cardinality, asymmetry and irreflexivity on a concrete pair — and the datatype tail, where +0.0 and -0.0 on a functional float property is a contradiction a human reader will never see and a value-space reasoner must. Les familles manquées par le fragment méritent d'être nommées, car c'est là qu'une ontologie casse en pratique : les contradictions au niveau des individus plutôt qu'entre classes — assertions négatives de propriété, individus mutuellement distincts, ensembles disjoints de classes et de propriétés, cardinalité maximale nulle, asymétrie et irréflexivité sur une paire concrète — et la queue des types de données, où +0.0 et -0.0 sur une propriété flottante fonctionnelle forment une contradiction qu'un lecteur humain ne verra jamais et qu'un raisonneur sur l'espace de valeurs doit voir.

Verify this yourself Vérifiez-le vous-même

Every figure on this page is reproducible with the published ontologies and two Rust tools. Load the corpus into a store, then ask whether an entailed membership holds: Chaque chiffre de cette page est reproductible avec les ontologies publiées et deux outils Rust. Chargez le corpus dans un magasin, puis demandez si une appartenance entraînée tient :

oxigraph load --location ./store --file edgy.ttl
oxigraph load --location ./store --file edgy-bfo-2020.ttl
oxigraph query --location ./store --query \
  'PREFIX edgy: <https://schema.bra0.org/cross-domain/edgy#>
   ASK { <urn:x> a edgy:Organization }'
# false — and the three axioms that entail it are in the store

Then reproduce the asymmetry. Ask the reasoner about a premise the W3C suite declares unsatisfiable, and about one of our own seeded contradictions, and compare what each answer is worth. Pass a time bound on every call: one of the suite's own cases does not terminate. Reproduisez ensuite l'asymétrie. Interrogez le raisonneur sur une prémisse que la suite W3C déclare insatisfiable, puis sur l'une de nos contradictions semées, et comparez ce que vaut chaque réponse. Passez une borne de temps à chaque appel : un cas de la suite elle-même ne termine pas.

# a contradiction between two classes — the engine finds it
rustdl consistent --json seeded-disjoint.ofn
# {"consistent": false, ...}        <- evidence: it found something

# a contradiction between two float values on a functional property
rustdl consistent --json Plus_and_Minus_Zero_are_Distinct.ofn
# {"consistent": true, "incomplete": false, "dropped": {}}
#                 ^^^^ not evidence: it found nothing, and nothing
#                      in the contract says it could have

# so always bound the call, and never arm a gate on the true
./guard.sh 25 rustdl consistent --json <premise>

Measured 2026-10-17 over 343 files and 33 242 triples of the live corpus.