Concept : SW-13 a comparé les raisonneurs OWL (owlrl, HermiT, reasonable) — tous répondent oui ou non, aucun n’explique pourquoi il le croit. Ce notebook introduit le proof-carrying inference : chaque conclusion s’accompagne d’un certificat qu’un checker indépendant accepte ou rejette. Le concept est incarné par la plateforme open-ontologies (Fabio Rovai, MIT, moteur Rust + checkers Lean 4 prouvés sound, préprint arXiv:2605.09184), dont le README s’ouvre sur une phrase qui vaut un cours :
Ask a reasoner why it believes something and it will tell you to trust it. This one hands you the proof, and refuses a fake one. (« Demandez à un raisonneur pourquoi il croit quelque chose, il vous répondra de lui faire confiance. Celui-ci vous tend la preuve, et refuse une preuve forgée. »)
Plan :
Contexte — le gap de SW-13 et la table fil rouge « avec une preuve / sans preuve » ;
L’ontologie jouet et le moteur Horn naïf — forward chaining qui enregistre pourquoi ;
Le certificat d’inférence — un artefact transportable, vérifiable par un tiers ;
Le checker indépendant — vérifie, ne re-déduit pas ; verdicts et rejets nommés ;
Quatre forges rejetées — le résultat falsifiable ;
La jambe réelle — le binaire open-ontologies v1.4.0 sur l’ontologie pizza de la série, et notre checker jouet qui vérifie son vrai certificat ;
Ce que le certificat NE prouve PAS — les limites load-bearing, écrites ;
L’honnêteté documentaire — le commit 55abe97 comme cas d’étude ;
Table fil rouge finale et cross-links — vericode, Z3, Tweety, Lean.
Objectifs d’apprentissage
À la fin de ce notebook, vous saurez :
expliquer pourquoi une conclusion de raisonneur sans preuve transportable est un acte de confiance, pas un fait vérifiable ;
implémenter un moteur Horn naïf qui émet une étape de dérivation par inférence ;
écrire un checker indépendant de certificats (unification, disponibilité ordonnée des prémisses, auto-support) qui rejette nommément les certificats forgés ;
distinguer les verdicts entailed et entailed_under_supplied_rules — une règle que vous avez écrite est une supposition, jamais un fait ;
invoquer le vrai binaire open-ontologies (tag figé, SHA256 vérifié) et vérifier son certificat oo-cert/1 ;
énoncer ce qu’un certificat ne prouve pas : provenance des assertions, moteurs partageant le même algorithme, théorème cité mais non machine-checké.
SW-13 a benchmarké owlrl, HermiT (via OWLReady2), reasonable : temps d’exécution, nombre de triplets inférés, facilité d’installation. Ce que le benchmark ne pouvait pas mesurer, c’est la nature de la réponse. Interrogez owlrl sur « margherita est-elle un aliment ? », il matérialise le triplet — et si vous lui demandez pourquoi, la réponse est dans le code du moteur, pas dans un artefact que vous pourriez transmettre à un tiers. Un grep de certificate, proof ou justif dans SW-13 rend zéro résultat : le concept même de preuve transportable est absent — c’est le gap que ce notebook comble.
L’idée a un précédent célèbre côté langages : le proof-carrying code (Necula, 1997), où un compilateur non fiable accompagne chaque binaire d’une preuve qu’un checker minuscule — et donc auditable — valide avant d’exécuter. open-ontologies transpose ce geste au Web Sémantique : le raisonneur (Rust, ou un moteur Python pur) n’est pas fiable, mais chaque inférence s’accompagne d’un certificat qu’un checker écrit en Lean 4 — dont la correction est un théorème machine-checké (OOCert.certificate_sound) — accepte ou rejette :
flowchart LR
E["Moteur non fiable<br/>Rust, ou le jouet Python de ce notebook"] -->|certificat| C["Checker indépendant<br/>Lean 4 (théorème), ou jouet Python (procédure)"]
C -->|règles intégrées| A["entailed"]
C -->|règles fournies| B["entailed_under_supplied_rules"]
C -->|certificat forgé| X["rejeté, raison nommée"]
La table fil rouge — avec une preuve, sans une preuve
Cette table reviendra en fin de notebook (section 9), enrichie par ce que nous aurons mesuré. Elle est l’ossature du cours :
Question
Sans preuve (statut quo SW-13)
Avec un certificat (ce notebook)
Pourquoi croire à la conclusion ?
« le raisonneur l’a dit »
une suite d’étapes, chacune relue
Un tiers peut vérifier ?
non — il doit ré-exécuter le même moteur
oui — le fichier suffit, le moteur n’intervient plus
Une conclusion peut-elle être forgée ?
indétectable
rejet nommé (premisse absente, auto-support, liaison incohérente…)
Une règle métier change-t-elle le statut ?
non distingué
oui — entailed_under_supplied_rules ≠ entailed
Que prouve le « non » ?
rien (opinion d’oracle)
rien non plus — c’est une limite écrite (section 7)
2. L’ontologie jouet et le moteur Horn naïf
Le domaine rejoint la fixture pizza de la série (data/pizza.owl, utilisée par SW-7 et SW-13) en miniature : une pizzeria, des ingrédients, des allergènes. Neuf triplets assertés, quatre règles Horn sur motifs de triplets — trois règles RDFS « intégrées » (rdfs9, rdfs11, rdfs3) et une règle métier écrite par nous (allergenPropagation : si une pizza contient un ingrédient qui porte un allergène, la pizza porte l’allergène).
Notation : un triplet est un tuple (sujet, prédicat, objet) d’IRIs ; une règle a des prémisses et une conclusion qui sont des patrons de triplets, où les variables commencent par ?. Exemple rdfs9 — la propagation de type par sous-classe :
La distinction règle intégrée / règle fournie n’est pas cosmétique : nous verrons au checker qu’elle change le verdict — c’est exactement la sémantique d’open-ontologies, où une règle que vous avez écrite est une supposition que le certificat transporte, jamais un fait qu’il établit.
# L'ontologie jouet : faits assertés + table de règles Horn.RDF_TYPE ="http://www.w3.org/1999/02/22-rdf-syntax-ns#type"RDFS_SUBCLASS ="http://www.w3.org/2000/01/rdf-schema#subClassOf"RDFS_RANGE ="http://www.w3.org/2000/01/rdf-schema#range"EX ="http://example.org/pizza#"def q(local: str) ->str:# Raccourci d'IRI dans le vocabulaire de la pizzeria.return EX + localasserted = [# instances (q("margherita"), RDF_TYPE, q("NamedPizza")), (q("margherita"), q("containsIngredient"), q("mozzarella")), (q("mozzarella"), q("hasAllergen"), q("milk")), (q("mozzarella"), RDF_TYPE, q("DairyProduct")),# hiérarchie de classes (q("NamedPizza"), RDFS_SUBCLASS, q("Pizza")), (q("Pizza"), RDFS_SUBCLASS, q("Food")), (q("Food"), RDFS_SUBCLASS, q("Consumable")), (q("DairyProduct"), RDFS_SUBCLASS, q("AllergenSource")),# schéma : portée de hasAllergen (q("hasAllergen"), RDFS_RANGE, q("Allergen")),]rules = {"rdfs9": { # intégrée — type hérite des super-classes"premises": [("?x", RDF_TYPE, "?c"), ("?c", RDFS_SUBCLASS, "?d")],"conclusion": ("?x", RDF_TYPE, "?d")},"rdfs11": { # intégrée — subClassOf est transitif"premises": [("?a", RDFS_SUBCLASS, "?b"), ("?b", RDFS_SUBCLASS, "?c")],"conclusion": ("?a", RDFS_SUBCLASS, "?c")},"rdfs3": { # intégrée — la portée (range) type l'objet"premises": [("?p", RDFS_RANGE, "?c"), ("?x", "?p", "?y")],"conclusion": ("?y", RDF_TYPE, "?c")},"allergenPropagation": { # FOURNIE — règle métier écrite par nous"premises": [("?pizza", q("containsIngredient"), "?ing"), ("?ing", q("hasAllergen"), "?all")],"conclusion": ("?pizza", q("hasAllergen"), "?all")},}BUILTIN_RULES = {"rdfs9", "rdfs11", "rdfs3"}print(f"Faits assertés : {len(asserted)}")print(f"Règles : {len(rules)} (intégrées : {sorted(BUILTIN_RULES)} ; "f"fournie : allergenPropagation)")for name, r in rules.items(): prem =" ; ".join(f"({p[0]}{p[1].split('#')[-1].split('/')[-1]}{p[2]})"for p in r["premises"]) concl =f"({r['conclusion'][0]}{r['conclusion'][1].split('#')[-1].split('/')[-1]}{r['conclusion'][2]})"print(f" {name:<20}{prem} => {concl}")
Le moteur naïf : forward chaining qui enregistre le pourquoi
L’algorithme est volontairement naïf — ce n’est pas lui qui doit être subtil, c’est le certificat. À chaque tour, on essaie d’unifier les prémisses de chaque règle avec les triplets déjà connus ; chaque inférence nouvelle est ajoutée et enregistrée comme une étape de dérivation : la règle, la conclusion, les prémisses concrètes qui l’ont produite. On s’arrête au point fixe.
C’est la seule différence avec la clôture owlrl de SW-13 : owlrl rend un ensemble de triplets inférés ; ici, chaque triplet inféré arrive avec son pourquoi. Une variable liée deux fois à des valeurs différentes échoue (décision 0008 d’open-ontologies : a binding is data and evidence admits one reading).
# Moteur Horn naïf : forward chaining avec émission d'étapes de dérivation.def match(template, triple):# Unifie un triplet-patron avec un triplet ground ; renvoie {var: terme} ou None. subst = {}for t, g inzip(template, triple):ifisinstance(t, str) and t.startswith("?"):if t in subst and subst[t] != g:returnNone# variable liée deux fois à des valeurs différentes subst[t] = gelif t != g:returnNonereturn substdef forward_chain(asserted, rules, max_iter=20):# Forward chaining jusqu'au point fixe ; chaque inférence émet une étape. known =list(asserted) derivations = [] changed, iterations =True, 0while changed and iterations < max_iter: changed =False iterations +=1for name, rule in rules.items():for triple inlist(known): s1 = match(rule["premises"][0], triple)if s1 isNone:continueiflen(rule["premises"]) ==1: concl =tuple(s1.get(t, t) for t in rule["conclusion"])if concl notin known: known.append(concl) derivations.append({"rule": name, "conclusion": concl,"premises": [triple]}) changed =Truecontinuefor t2 in known: s2 = match(tuple(s1.get(t, t) for t in rule["premises"][1]), t2)if s2 isNone:continue subst = {**s1, **s2} concl =tuple(subst.get(t, t) for t in rule["conclusion"])if concl notin known: known.append(concl) derivations.append({"rule": name, "conclusion": concl,"premises": [triple, t2]}) changed =Truereturn known, derivations, iterationsknown, derivations, iterations = forward_chain(asserted, rules)court =lambda t: "/".join(x.split("#")[-1].split("/")[-1] for x in t)print(f"Faits assertés : {len(asserted)}")print(f"Faits au point fixe : {len(known)} ({len(derivations)} inférences, {iterations} itérations)")print("\nÉtapes de dérivation émises :")for i, d inenumerate(derivations): prem =" ; ".join(court(p) for p in d["premises"])print(f" [{i}] {d['rule']:<20}{court(d['conclusion'])}")print(f" <- {prem}")
Sortie obtenue : 9 faits assertés, 18 faits au point fixe, 9 inférences en 3 itérations.
Aspect
Valeur
Signification
Inférences
9
le moteur produit du nouveau connaissable sans nous
Itérations
3
la chaîne NamedPizza → Pizza → Food → Consumable exige plusieurs tours
Étapes multi-sauts
dérivations 6, 7, 8
leur prémisses sont elles-mêmes dérivées (ex. [7] margherita/type/Consumable utilise [0] margherita/type/Pizza et [3] Pizza/subClassOf/Consumable)
Règle métier
[5] margherita/hasAllergen/milk
produite par allergenPropagation, la règle que nous avons écrite
La conclusion « margherita est un allergène au lait » est vraie pour ce moteur. Mais la sortie ci-dessus est une liste imprimée : un tiers qui ne fait pas confiance au moteur ne peut rien en faire — il devrait ré-exécuter le même code, c’est-à-dire faire le même acte de confiance que celui qu’on voulait éviter. C’est précisément le problème que le certificat résout.
3. Émettre le certificat
Un certificat d’inférence est un fichier autonome contenant tout ce qu’un tiers doit connaître pour juger la conclusion — et rien d’autre :
la table de règles (patrons de prémisses/conclusion) ;
les faits assertés (le point de départ, tel que le certificat le déclare — voir la limite de provenance en section 7) ;
les étapes de dérivation ordonnées : règle, conclusion ground, prémisses ground ;
la claim à certifier.
Le format jouet est JSON (sw16-toy-cert/1). open-ontologies utilise le même contenu en TSV (oo-cert/1 : règle <TAB> s p o <TAB> prémisses…) — nous le vérifierons tel quel en section 6. La propriété décisive : vérifier ne coûte pas plus que lire — aucun raisonnement, aucune recherche de point fixe, juste une relecture d’étapes déjà écrites.
# Émission du certificat : le moteur sérialise règles + faits + dérivations.WORK = Path("sw16-work")WORK.mkdir(exist_ok=True)certificate = {"format": "sw16-toy-cert/1","rule_table": {name: {"premises": [list(p) for p in r["premises"]],"conclusion": list(r["conclusion"])}for name, r in rules.items()},"asserted": [list(t) for t in asserted],"derivations": [{"rule": d["rule"], "conclusion": list(d["conclusion"]),"premises": [list(p) for p in d["premises"]]}for d in derivations],}cert_path = WORK /"certificat-margherita.json"cert_path.write_text(json.dumps(certificate, indent=1, ensure_ascii=False), encoding="utf-8")print(f"Certificat écrit : {cert_path} ({cert_path.stat().st_size} octets)")print(f" format : {certificate['format']}")print(f" règles : {len(certificate['rule_table'])}")print(f" assertés : {len(certificate['asserted'])}")print(f" dérivations : {len(certificate['derivations'])}")der7 = certificate["derivations"][7]print(f"\nExemple — étape 7 (multi-sauts, prémisses dérivées) :")print(f" règle : {der7['rule']}")print(f" conclusion : {court(tuple(der7['conclusion']))}")for p in der7["premises"]:print(f" prémisses : {court(tuple(p))}")
Sortie obtenue : le fichier sw16-work/certificat-margherita.json porte la table de règles, les 9 faits assertés et les 9 dérivations ordonnées.
L’étape 7 rend visible la chaîne multi-sauts : sa prémisses margherita/type/Pizza n’est pas un fait asserté — c’est la conclusion de l’étape 0. Le fichier est donc auto-porteur : qui le lit voit où chaque prémisses a été obtenue (assertée, ou dérivée plus haut), sans jamais rouvrir le moteur. C’est ce fichier — et lui seul — que la section suivante va juger.
4. Le checker indépendant
Le checker ne re-déduit rien : aucun point fixe, aucune recherche de règles applicables. Il relit chaque étape du certificat contre quatre exigences :
Règle connue — l’étape cite une règle de la table ;
Une seule substitution — les prémisses ground unifient avec les patrons sous une même liaison des variables, et la conclusion est exactement le patron de conclusion sous cette liaison (ground : plus aucune variable) ;
Disponibilité ordonnée — chaque prémisses est un fait asserté ou la conclusion d’une étape strictement antérieure. Interdit donc : l’auto-support (une étape qui se prend pour prémisses) et la prémisses du futur (une étape qui s’appuie sur ce qui sera prouvé plus bas) ;
Claim atteinte — la claim est la conclusion d’une étape acceptée.
Et l’indépendance n’est pas qu’une intention : le checker ci-dessous porte sa propre unification (lier_patron_checker), écrite sans appeler la moindre fonction du moteur — ni match, ni forward_chain. La cellule le prouve mécaniquement en inspectant le bytecode du checker : aucun nom du moteur n’y figure. Un buggy moteur ne peut donc pas contaminer la vérification par un helper partagé.
Deux verdicts positifs, calqués sur la sémantique d’open-ontologies : entailed si seules des règles intégrées soutiennent la claim ; entailed_under_supplied_rules si une règle fournie intervient — une règle que vous avez écrite est une supposition que le certificat transporte, jamais un fait qu’il établit. Un verdict négatif est rejected avec des raisons nommées.
# Checker indépendant : vérifie le certificat, ne re-déduit rien.def lier_patron_checker(patron, ground):# Unification propre au CHECKER — aucun appel au moteur (pas de match()).# Renvoie {variable: terme} si le triplet ground incarne le patron, sinon None. liaison = {}for p, g inzip(patron, ground):ifisinstance(p, str) and p.startswith("?"):if p in liaison and liaison[p] != g:returnNone# variable liée deux fois à des valeurs différentes liaison[p] = gelif p != g:returnNone# terme constant : égalité strictereturn liaisondef rules_reaching(cert, claim):# Marche arrière : quelles règles soutiennent (transitivement) la claim. concl_to_idx = {}for i, d inenumerate(cert["derivations"]): concl_to_idx.setdefault(tuple(d["conclusion"]), []).append(i) used, stack, seen =set(), [tuple(claim)], set()while stack: t = stack.pop()if t in seen:continue seen.add(t)for i in concl_to_idx.get(t, []): d = cert["derivations"][i] used.add(d["rule"])for p in d["premises"]: stack.append(tuple(p))return useddef check_certificate(cert, claim, builtin_rules):# Accepte ou rejette ; les rejets portent des raisons nommées. problems = [] rules_c = {n: {"premises": [tuple(p) for p in r["premises"]],"conclusion": tuple(r["conclusion"])}for n, r in cert["rule_table"].items()} available =set(tuple(t) for t in cert["asserted"])for i, d inenumerate(cert["derivations"]): name = d["rule"]if name notin rules_c: problems.append((i, name, "UNKNOWN_RULE"));continue rule = rules_c[name] prem_g = [tuple(p) for p in d["premises"]] concl_g =tuple(d["conclusion"])if (len(prem_g) !=len(rule["premises"]) orany(len(p) !=3for p in prem_g)orlen(concl_g) !=3): problems.append((i, name, "MALFORMED_STEP"));continue subst, ok_u = {}, Truefor t, g inzip(rule["premises"], prem_g): s = lier_patron_checker(t, g)if s isNone: ok_u =False; problems.append((i, name, "UNIFICATION_FAILED"));breakfor k, v in s.items():if subst.get(k, v) != v: ok_u =False; problems.append((i, name, "INCONSISTENT_BINDING"));breakifnot ok_u:break subst.update(s)ifnot ok_u:continue expected =tuple(subst.get(t, t) for t in rule["conclusion"])if concl_g != expected: problems.append((i, name, "CONCLUSION_MISMATCH"));continueifany(isinstance(x, str) and x.startswith("?") for x in concl_g): problems.append((i, name, "NON_GROUND_CONCLUSION"));continuefor p in prem_g:if p == concl_g: problems.append((i, name, "SELF_SUPPORT"))elif p notin available: problems.append((i, name, "PREMISE_NOT_AVAILABLE"))# Une étape invalide ne contribue PAS sa conclusion : les étapes# suivantes ne peuvent pas s'appuyer sur un fait mal établi.ifnotany(pi == i for pi, _, _ in problems): available.add(concl_g) claim_t =tuple(claim)if problems: vus, uniques =set(), []for prob in problems:if prob notin vus: vus.add(prob); uniques.append(prob)return {"ok": False, "verdict": "rejected","problems": [f"étape {i} [{r}] : {w}"for i, r, w in uniques],"claim_supported": claim_t in available}if claim_t notin available:return {"ok": False, "verdict": "rejected", "problems": ["CLAIM_NOT_DERIVED"],"claim_supported": False} used = rules_reaching(cert, claim_t) verdict ="entailed"if used <= builtin_rules else"entailed_under_supplied_rules"return {"ok": True, "verdict": verdict, "problems": [],"claim_supported": True, "rules_used": sorted(used)}# Preuve mécanique du découplage : le bytecode du checker ne référence# AUCUNE fonction du moteur — ni l'unification match(), ni forward_chain().assert"match"notin check_certificate.__code__.co_names, "checker -> moteur !"assert"forward_chain"notin check_certificate.__code__.co_namesprint("Découplage vérifié : check_certificate n'appelle aucune fonction du moteur ""(unification propre : lier_patron_checker).")claim_allergene = (q("margherita"), q("hasAllergen"), q("milk"))claim_type = (q("margherita"), RDF_TYPE, q("Consumable"))print("Claim 1 — margherita/hasAllergen/milk (règle métier impliquée) :")print(" ", json.dumps(check_certificate(certificate, claim_allergene, BUILTIN_RULES), ensure_ascii=False))print("Claim 2 — margherita/type/Consumable (règles intégrées seules) :")print(" ", json.dumps(check_certificate(certificate, claim_type, BUILTIN_RULES), ensure_ascii=False))
Sortie obtenue : la claim allergène reçoit entailed_under_supplied_rules avec rules_used: ["allergenPropagation"] ; la claim de type reçoit entailed avec rules_used: ["rdfs11", "rdfs9"].
Claim
Verdict
Pourquoi
margherita/hasAllergen/milk
entailed_under_supplied_rules
la marche arrière ne trouve que allergenPropagation — une règle fournie
margherita/type/Consumable
entailed
uniquement des règles intégrées (rdfs9, rdfs11) — vrai dans tout modèle du graphe asserté
Cette distinction est une fonctionnalité d’honnêteté, pas un détail : elle empêche la règle métier de se déguiser en fait établi. open-ontologies pousse la même exigence jusqu’au test — un test échoue si le verdict cesse de changer quand une règle fournie entre en jeu. Le fil rouge s’enrichit : sans preuve, ces deux claims auraient le même statut (« le raisonneur l’a dit »).
5. Tests négatifs — quatre certificats forgés, quatre rejets nommés
Un checker qui accepterait tout serait décoratif : la valeur se démontre en essayant de le tromper. Chaque forge ci-dessous est une attaque nommée contre une exigence du checker :
Forge
Attaque
Exigence visée
A — allergène fabriqué
ajoute « margherita porte le gluten » avec une prémisses inventée (mozzarella/hasAllergen/gluten, jamais assertée ni dérivée)
disponibilité des prémisses
B — auto-support
« la classe Spicy est sous-classe d’elle-même » en se prenant elle-même pour prémisses
pas de circularité
C — règle trompeuse
une dérivation étiquetée rdfs9 dont les prémisses sont celles de allergenPropagation
une seule substitution
D — prémisses du futur
la chaîne multi-sauts est réordonnée : l’étape 7 placée avant l’étape 0 dont elle dépend
disponibilité ordonnée
La forge D reproduit en miniature la classe de défauts que le différentiel multi-kernels d’open-ontologies a réellement attrapés sur son propre moteur (README v1.4.0 : cinq « false cleans », une règle concluant un triplet non sérialisable, deux kernels en désaccord sur des certificats pourtant valides de part et d’autre).
# Quatre forges, quatre rejets nommés — le résultat falsifiable.import copydef forge_ajout(cert, etape): f = copy.deepcopy(cert) f["derivations"].append(etape)return fforgeA = forge_ajout(certificate, {"rule": "allergenPropagation","conclusion": [q("margherita"), q("hasAllergen"), q("gluten")],"premises": [[q("margherita"), q("containsIngredient"), q("mozzarella")], [q("mozzarella"), q("hasAllergen"), q("gluten")]]})forgeB = forge_ajout(certificate, {"rule": "rdfs11","conclusion": [q("Spicy"), RDFS_SUBCLASS, q("Spicy")],"premises": [[q("Spicy"), RDFS_SUBCLASS, q("Spicy")], [q("Spicy"), RDFS_SUBCLASS, q("Spicy")]]})forgeC = forge_ajout(certificate, {"rule": "rdfs9","conclusion": [q("margherita"), RDF_TYPE, q("AllergenSource")],"premises": [[q("margherita"), q("containsIngredient"), q("mozzarella")], [q("mozzarella"), q("hasAllergen"), q("milk")]]})forgeD = copy.deepcopy(certificate)d = forgeD["derivations"]d[0], d[7] = d[7], d[0] # l'étape 7 passe AVANT l'étape 0 dont elle utilise la conclusionfor nom, forge, claim in [ ("Forge A — allergène fabriqué", forgeA, (q("margherita"), q("hasAllergen"), q("gluten"))), ("Forge B — auto-support", forgeB, claim_allergene), ("Forge C — règle trompeuse", forgeC, claim_allergene), ("Forge D — prémisses du futur", forgeD, claim_allergene),]: verdict = check_certificate(forge, claim, BUILTIN_RULES)print(f"{nom} : verdict = {verdict['verdict'].upper()}")for p in verdict["problems"]:print(f" REJET — {p}")
Sortie obtenue : les quatre forges sont rejetées, chacune pour une raison nommée — PREMISE_NOT_AVAILABLE (A), SELF_SUPPORT (B), UNIFICATION_FAILED (C), PREMISE_NOT_AVAILABLE sur l’étape 0 réordonnée (D).
Forge
Raison du rejet
Ce que le checker vient de prouver
A
PREMISE_NOT_AVAILABLE
on ne fabrique pas un fait en inventant une prémisses
B
SELF_SUPPORT
une preuve ne peut pas se prendre elle-même pour point de départ
C
UNIFICATION_FAILED
coller l’étiquette d’une règle intégrée sur des prémisses étrangères ne passe pas
D
PREMISE_NOT_AVAILABLE (étape 0)
l’ordre du certificat porte du sens : une étape ne peut s’appuyer que sur ce qui est déjà établi
Deux remarques d’honnêteté. D’abord, ces forges attaquent le certificat ; le moteur, lui, reste non fiable par hypothèse — c’est le régime de preuve-carrying : l’incrédulité envers le moteur est le point de départ, pas un accident. Ensuite, notre checker jouet partage le fichier avec le moteur dans ce notebook ; l’indépendance réelle — deux langages, deux historiques de code, un théorème de correction — est celle du checker Lean face au moteur Rust, que la section 6 cite à titre de jambe réelle.
Exemple guidé 1 — Étendre l’ontologie et certifier une nouvelle claim
Situation : la pizzeria ajoute la sauce tomate à sa margherita, et la sauce tomate porte l’allergène nightshade (famille des solanacées). Nous déroulons le cycle complet ensemble — l’exercice 1 ci-dessous interrogera le checker sous un angle que cet exemple ne couvre pas : les claims absentes.
Étendre asserted avec quatre faits : margherita containsIngredient tomatoSauce, tomatoSauce hasAllergen nightshade, tomatoSauce type VegetableProduct et VegetableProduct subClassOf AllergenSource ;
relancer le moteur et émettre le certificat étendu ;
vérifier avec check_certificate la claim margherita/hasAllergen/nightshade — quel verdict, et pourquoi ;
vérifier la claim tomatoSauce/type/AllergenSource — quel verdict, et quelle différence avec (c) ?
Indice de lecture : le verdict dépend de la marche arrière rules_reaching — quelles règles soutiennent chaque claim ?
# Exemple guidé 1 — ontologie étendue, certificat émis, deux verdicts.asserted_ex1 = asserted + [ (q("margherita"), q("containsIngredient"), q("tomatoSauce")), (q("tomatoSauce"), q("hasAllergen"), q("nightshade")), (q("tomatoSauce"), RDF_TYPE, q("VegetableProduct")), (q("VegetableProduct"), RDFS_SUBCLASS, q("AllergenSource")),]known_ex1, derivations_ex1, iters_ex1 = forward_chain(asserted_ex1, rules)certificat_ex1 = {"format": "sw16-toy-cert/1","rule_table": {name: {"premises": [list(p) for p in r["premises"]],"conclusion": list(r["conclusion"])}for name, r in rules.items()},"asserted": [list(t) for t in asserted_ex1],"derivations": [{"rule": d["rule"], "conclusion": list(d["conclusion"]),"premises": [list(p) for p in d["premises"]]}for d in derivations_ex1],}print(f"Ontologie étendue : {len(asserted_ex1)} assertés, "f"{len(derivations_ex1)} dérivations en {iters_ex1} itérations")claim_nightshade = (q("margherita"), q("hasAllergen"), q("nightshade"))claim_veg = (q("tomatoSauce"), RDF_TYPE, q("AllergenSource"))v1 = check_certificate(certificat_ex1, claim_nightshade, BUILTIN_RULES)v2 = check_certificate(certificat_ex1, claim_veg, BUILTIN_RULES)print("Claim (c) margherita/hasAllergen/nightshade :", json.dumps(v1, ensure_ascii=False))print("Claim (d) tomatoSauce/type/AllergenSource :", json.dumps(v2, ensure_ascii=False))
Lecture — Exemple guidé 1 : deux statuts épistémiques dans un même fichier
La claim (c) reçoit entailed_under_supplied_rules — elle repose sur allergenPropagation, une règle fournie. La claim (d) reçoit entailed — elle ne mobilise que rdfs9 sur des faits assertés. Le même certificat porte donc deux statuts épistémiques différents, lisibles dans le fichier : c’est toute la différence avec SW-13, où les deux conclusions seraient de simples triplets inférés, indiscernables.
Exercice 1 — Une claim absente : que répond le checker, exactement ?
Contexte : l’exemple guidé 1 n’a interrogé le checker que sur des claims soutenues. Un checker honnête doit aussi répondre — correctement — quand on lui demande une claim qui n’est pas dans le certificat, ou une claim qui n’y figure que comme fait asserté, jamais dérivée.
Objectif : sur le certificat honnête certificate de la section 3, sans rien lui ajouter, exécuter check_certificate sur deux claims et interpréter la différence :
la claim (margherita, hasAllergen, gluten) — le gluten ne figure nulle part dans l’ontologie. Verdict, problems, claim_supported ? Notez la forme de ce rejet : c’est le seul qui ne cite aucune étape ;
la claim (mozzarella, hasAllergen, milk) — un fait asserté, jamais dérivé. Verdict, et que vaut rules_used ?
en une phrase : pourquoi le checker répond-il rejected plutôt que « cette claim est fausse » — qu’est-ce que le checker ne sait tout simplement pas dire ?
Indice : suivez le code de check_certificate APRÈS la boucle sur les étapes — que se passe-t-il quand problems est vide mais que la claim n’est pas dans available ? Et pour (b), que renvoie rules_reaching quand aucune dérivation ne conclut le triplet ? - Etape 1 : v1 = check_certificate(certificate, (q(“margherita”), q(“hasAllergen”), q(“gluten”)), BUILTIN_RULES) - Etape 2 : v2 = check_certificate(certificate, (q(“mozzarella”), q(“hasAllergen”), q(“milk”)), BUILTIN_RULES) - Etape 3 : lire verdict / problems / rules_used de chacun, puis formuler (c)
# Exercice 1 — à compléter# Etape 1 : la claim absente (gluten) sur le certificat honnête# Etape 2 : la claim assertée jamais dérivée (mozzarella/lait)# Etape 3 : lecture des verdicts et réponse à (c)resultat_ex1 =None# TODO étudiant : (verdict gluten, verdict mozzarella, réponse à (c))print("Exercice 1 à compléter")
Exercice 1 à compléter
6. La jambe réelle — le binaire open-ontologies v1.4.0
Le jouet démontre le concept ; la comparaison exige le vrai outil. open-ontologies (Fabio Rovai, MIT) est une plateforme d’ingénierie et de vérification d’ontologies : moteur de raisonnement Rust, checkers Lean 4 dont la correction est machine-checkée, second kernel Isabelle, studio web — et un préprint (arXiv:2605.09184). Le dépôt évolue vite : toute utilisation fige le tag. Ici :
Résolution du binaire (dans l’ordre) : variable d’environnement OPEN_ONTOLOGIES_BIN → ext_tools/ local à la série → PATH → téléchargement automatique depuis l’URL épinglée de la release (58 Mo, une seule fois, puis cache). Le SHA256 est recontrôlé à chaque résolution : un binaire dont l’empreinte ne correspond pas au pin n’est pas invoqué.
# Résolution (ou installation) du binaire épinglé v1.4.0 — règle : installer, jamais contourner.PINNED_VERSION ="v1.4.0"PINNED_SHA256 = {"open-ontologies-x86_64-pc-windows-msvc.exe": "e1e1334408227d208837de1b389b6b9aad24cc87b825de8c28480f2c39b210d5","open-ontologies-x86_64-unknown-linux-gnu": "8cdc57af888a9a0578ccb3646dfc28757cbb533d155f368788b7df5543a7ef56","open-ontologies-aarch64-apple-darwin": "85db2eadd74331eaca51fd8b535e51ea8ecb9dfb396cae46fdc087ba3c84ee63","open-ontologies-x86_64-apple-darwin": "ddbdb980c24a57a93c65edf08d3bfa515843148f61e7a9bc8b6c8aeda7afa55c",}_mach = platform.machine().lower()ASSET =Noneif os.name =="nt": ASSET ="open-ontologies-x86_64-pc-windows-msvc.exe"elif sys.platform =="darwin": ASSET = ("open-ontologies-aarch64-apple-darwin"if _mach in ("arm64", "aarch64")else"open-ontologies-x86_64-apple-darwin")elif sys.platform.startswith("linux"): ASSET ="open-ontologies-x86_64-unknown-linux-gnu"assert ASSET isnotNone, f"plateforme non supportée par les releases : {sys.platform}"PINNED_URL =f"https://github.com/fabio-rovai/open-ontologies/releases/download/{PINNED_VERSION}/{ASSET}"def sha256_fichier(path: Path) ->str:# Empreinte SHA256 d'un fichier, en une lecture. h = hashlib.sha256() h.update(path.read_bytes())return h.hexdigest()def resoudre_binaire() -> Path:# env OPEN_ONTOLOGIES_BIN -> ext_tools/ -> PATH -> téléchargement épinglé. env = os.environ.get("OPEN_ONTOLOGIES_BIN")if env and Path(env).is_file():return Path(env) local = Path("ext_tools") / ASSETif local.is_file():return localfor cand in (Path(ASSET), Path(ASSET).with_suffix("")):if cand.is_file():return candprint(f"Binaire absent — téléchargement épinglé {PINNED_VERSION} (~58 Mo, une fois)…") local.parent.mkdir(exist_ok=True) urllib.request.urlretrieve(PINNED_URL, local)if os.name !="nt": local.chmod(0o755)return localOO_BIN = resoudre_binaire()empreinte = sha256_fichier(OO_BIN)attendue = PINNED_SHA256[ASSET]integrite_ok = empreinte == attendueprint(f"Binaire : {OO_BIN} ({OO_BIN.stat().st_size:,} octets)")print(f"SHA256 : {empreinte}")print(f"Attendu : {attendue}")print(f"Intégrité : {'OK — empreinte conforme au pin v1.4.0'if integrite_ok else'ÉCHEC — binaire non invoqué'}")
Binaire : ext_tools\open-ontologies-x86_64-pc-windows-msvc.exe (60,875,264 octets)
SHA256 : e1e1334408227d208837de1b389b6b9aad24cc87b825de8c28480f2c39b210d5
Attendu : e1e1334408227d208837de1b389b6b9aad24cc87b825de8c28480f2c39b210d5
Intégrité : OK — empreinte conforme au pin v1.4.0
Charger la vraie pizza et raisonner avec certificat
La fixture est data/pizza.owl — l’ontologie pizza canonique (co-ode) déjà livrée dans la série pour SW-7 et SW-13, donc une vraie ontologie, déjà sourcée, pas un exemple inventé. Le binaire fonctionne en batch : load puis reason --profile rdfs --certificate <dir> — le store étant en mémoire, les deux commandes doivent partager un même batch. La réponse JSON contient les compteurs, et le répertoire cible reçoit le certificat oo-cert/1 (asserted.tsv + derivations.tsv) que le champ check_with invite à faire vérifier par le checker Lean (lake exe oo-cert …).
# Jambe réelle : batch load + reason --certificate sur data/pizza.owl.ifnot integrite_ok:print("ÉCHEC d'intégrité du binaire — invocation refusée (pin SHA256 non conforme).")else: OO_DATA = WORK /"oo-data" CERT_PIZZA = WORK /"cert-pizza" shutil.rmtree(CERT_PIZZA, ignore_errors=True) batch = WORK /"batch-pizza.txt" batch.write_text(f"load data/pizza.owl\n"f"stats\n"f"reason --profile rdfs --certificate {CERT_PIZZA.as_posix()}\n", encoding="utf-8") proc = subprocess.run( [str(OO_BIN), "batch", str(batch), "--data-dir", str(OO_DATA), "--no-connect"], capture_output=True, text=True, encoding="utf-8", timeout=300) reponses = [json.loads(l) for l in proc.stdout.splitlines() if l.strip().startswith("{")]for r in reponses:if r["command"] =="load":print(f"load : {r['result']['triples_loaded']} triplets chargés")elif r["command"] =="stats": s = r["result"]print(f"stats : {s['triples']} triplets, {s['classes']} classes, "f"{s['individuals']} individus, {s['object_properties']} propriétés d'objet") raison =next(r for r in reponses if r["command"] =="reason")["result"] cert = raison["certificate"]print(f"reason: {raison['inferred_count']} inférences en {raison['iterations']} itérations "f"(point fixe : {raison['fixpoint_reached']})")print(f" par règle : {cert['by_rule']}")print(f" format : {cert['format']}")print(f" dérivations : {cert['derivations']} | assertés : {cert['asserted']}")print(f" vérif. Lean : {cert['check_with']}")
Sortie obtenue : la fixture charge 1944 triplets (99 classes, 218 individus) ; le profil rdfs dérive 258 inférences en 4 itérations, toutes par la règle rdfs11 (transitivité de subClassOf) ; le certificat oo-cert/1 est écrit avec 258 dérivations.
Aspect
Valeur mesurée
Signification
Triplets assertés
1944
vraie ontologie, déjà utilisée par SW-7/SW-13
Inférences
258
la hiérarchie de classes de la pizza est profonde — la transitivité travaille
Règles mobilisées
rdfs11 seule
sur cette ontologie, le profil RDFS ne tire que de la transitivité
Certificat
oo-cert/1, 258 étapes
le moteur émet les prémisses ground de chaque dérivation — même format d’idée que notre jouet
Vérification annoncée
lake exe oo-cert …
la jambe indépendante est le checker Lean (section 7 pour ses limites)
Note d’honnêteté (README v1.4.0) : « The proofs are ahead of the published release » — la couche vérifiée décrite dans le README vit sur main, plus récente que le tag ; le binaire de release embarque le moteur et l’émission de certificats, la preuve de correction du checker se lit dans lean/OOCert au tag. C’est exactement le genre de précision que la section 8 érige en discipline.
Notre checker jouet vérifie le certificat réel
Le format oo-cert/1 est un TSV : règle <TAB> s p o <TAB> s p o [<TAB> s p o] — règle, conclusion, puis une prémisses par groupe de trois (les mêmes informations que notre JSON jouet, sérialisées autrement). Notre check_oo_cert ci-dessous applique la même procédure (unification sous une seule substitution, disponibilité ordonnée) avec la même unification propre au checker (lier_patron_checker) — aucune fonction du moteur n’intervient ici non plus. Deux exécutions : le certificat tel qu’émis, puis une copie trafiquée (le sujet de la première conclusion est réécrit) — un checker qui n’accepterait que ne vaudrait rien.
# Vérification du certificat oo-cert/1 réel — puis d'une copie trafiquée.def check_oo_cert(asserted_path, derivations_path, rule_table):# Même procédure que check_certificate, sur le TSV oo-cert/1 —# et même unification propre au checker (lier_patron_checker, pas match). problems = []withopen(asserted_path, encoding="utf-8") as f: available =set(tuple(c.strip().strip("<>") for c in line.rstrip("\n").split("\t"))for line in f if line.strip()) n =0withopen(derivations_path, encoding="utf-8") as f:for i, line inenumerate(f):ifnot line.strip():continue n +=1 fields = line.rstrip("\n").split("\t") name, terms = fields[0], [c.strip().strip("<>") for c in fields[1:]]if name notin rule_table: problems.append((i, name, "UNKNOWN_RULE"));continue rule = rule_table[name] nprem =len(rule["premises"])iflen(terms) !=3* (1+ nprem): problems.append((i, name, "ARITY"));continue concl_g =tuple(terms[0:3]) prem_g = [tuple(terms[3+3* k: 6+3* k]) for k inrange(nprem)] subst, ok_u = {}, Truefor t, g inzip(rule["premises"], prem_g): s = lier_patron_checker(tuple(t), g)if s isNone: ok_u =False; problems.append((i, name, "UNIFICATION_FAILED"));breakfor k2, v2 in s.items():if subst.get(k2, v2) != v2: ok_u =False;breakifnot ok_u:break subst.update(s)ifnot ok_u: problems.append((i, name, "INCONSISTENT_BINDING"));continue expected =tuple(subst.get(t, t) for t in rule["conclusion"])if concl_g != expected: problems.append((i, name, "CONCLUSION_MISMATCH"));continuefor p in prem_g:if p == concl_g: problems.append((i, name, "SELF_SUPPORT"))elif p notin available: problems.append((i, name, "PREMISE_NOT_AVAILABLE"))# Une étape invalide ne contribue PAS sa conclusion.ifnotany(pi == i for pi, _, _ in problems): available.add(concl_g)return {"steps": n, "total_problems": len(problems),"reasons": sorted({w for _, _, w in problems}),"problems": [f"étape {i} [{r}] : {w}"for i, r, w in problems[:3]]}# Le checker TSV non plus ne référence aucune fonction du moteur.assert"match"notin check_oo_cert.__code__.co_names, "checker TSV -> moteur !"print("Découplage vérifié : check_oo_cert utilise lier_patron_checker, pas match().")OO_RULES = {"rdfs9": {"premises": [("?x", RDF_TYPE, "?c"), ("?c", RDFS_SUBCLASS, "?d")],"conclusion": ("?x", RDF_TYPE, "?d")},"rdfs11": {"premises": [("?a", RDFS_SUBCLASS, "?b"), ("?b", RDFS_SUBCLASS, "?c")],"conclusion": ("?a", RDFS_SUBCLASS, "?c")},}if integrite_ok: ok_cert = check_oo_cert(CERT_PIZZA /"asserted.tsv", CERT_PIZZA /"derivations.tsv", OO_RULES)print("Certificat réel tel qu'émis :", json.dumps(ok_cert, ensure_ascii=False))# Forge E : copie trafiquée — le sujet de la conclusion de l'étape 0 est réécrit# (suffixe FORGE inséré dans l'IRI, indépendant du contenu de la ligne). trafique_dir = WORK /"cert-pizza-trafique" shutil.rmtree(trafique_dir, ignore_errors=True) trafique_dir.mkdir() shutil.copy(CERT_PIZZA /"asserted.tsv", trafique_dir /"asserted.tsv") lignes = (CERT_PIZZA /"derivations.tsv").read_text(encoding="utf-8").splitlines() champs = lignes[0].split("\t") sujet = champs[1]assert sujet.startswith("<") and sujet.endswith(">"), sujet champs[1] = sujet[:-1] +"FORGE>"# <...quelquechoseFORGE> lignes[0] ="\t".join(champs) (trafique_dir /"derivations.tsv").write_text("\n".join(lignes) +"\n", encoding="utf-8") res_forge = check_oo_cert(trafique_dir /"asserted.tsv", trafique_dir /"derivations.tsv", OO_RULES)# Résumé INVARIANT de la forge E : ce que toute exécution doit donner.# total_problems, lui, est une MESURE DE RUN : l'ordre des dérivations du# binaire n'est pas stable (constaté firsthand : 2 problèmes sur un run, 1 sur un autre). rejete = res_forge["total_problems"] >=1 a_cm ="CONCLUSION_MISMATCH"in res_forge["reasons"]print("Forge E — certificat réel trafiqué — résumé invariant :")print(f" rejet : {rejete}")print(f" contient CONCLUSION_MISMATCH : {a_cm}")print(f" total_problems (mesure de CE run): {res_forge['total_problems']} — "f"variable entre exécutions, jamais une garantie")print(f" raisons observées : {res_forge['reasons']}")
Découplage vérifié : check_oo_cert utilise lier_patron_checker, pas match().
Certificat réel tel qu'émis : {"steps": 258, "total_problems": 0, "reasons": [], "problems": []}
Forge E — certificat réel trafiqué — résumé invariant :
rejet : True
contient CONCLUSION_MISMATCH : True
total_problems (mesure de CE run): 2 — variable entre exécutions, jamais une garantie
raisons observées : ['CONCLUSION_MISMATCH', 'PREMISE_NOT_AVAILABLE']
Interprétation — un checker de soixante lignes face à un moteur de production
Sortie obtenue : le certificat émis par le binaire passe intégralement (258 étapes, 0 problème) ; la copie trafiquée est rejetée, et le rejet contient CONCLUSION_MISMATCH — l’étape forgée (sujet suffixé FORGE) ne se reconstruit depuis aucune prémisses. C’est l’invariant que nous clamons, et rien de plus : le nombre de problèmes varie d’une exécution à l’autre, car l’ordre des dérivations du binaire n’est pas stable (constaté firsthand : deux problèmes sur une exécution, un seul sur la suivante). Quand une dérivation aval suit l’étape empoisonnée dans l’ordre du fichier, elle tombe en PREMISE_NOT_AVAILABLE — une cascade possible, jamais garantie. C’est pourquoi la cellule imprime un résumé stable : rejet + présence de CONCLUSION_MISMATCH, le total étant présenté comme mesure de run, pas comme promesse.
Ce qu’il faut en retenir — et ce qu’il ne faut pas en conclure :
Ce qui est démontré : le format certificat rend la vérification bon marché et indépendante du moteur. Le fichier ne demande ni Oxigraph, ni Rust, ni point fixe : soixante lignes de Python stdlib — avec leur propre unification — relisent les 258 dérivations, prémisses dérivées comprises (l’ordre du fichier suffit à justifier chaque chaîne).
Ce qui n’est PAS démontré : notre jouet applique la procédure de vérification, il ne porte aucun théorème. Chez open-ontologies, c’est le checker Lean qui est prouvé sound (OOCert.certificate_sound : si le checker accepte, alors la conclusion est vraie dans tout modèle du graphe asserté). Notre Python n’a pas d’équivalent — c’est un instrument pédagogique, pas une jambe de confiance.
Exemple guidé 2 — La forge de la double liaison (décision 0008)
Le README d’open-ontologies raconte une divergence réelle trouvée par son différentiel multi-kernels : deux checkers valides lisaient différemment un certificat dont une même variable était liée à deux valeurs différentes dans les prémisses — « A key bound twice to different values is satisfied by no substitution at all » (décision 0008 : a binding is data and evidence admits one reading). Nous forgeons cette attaque ensemble — l’exercice 2 ci-dessous attaquera par un autre versant : la table de règles elle-même.
construire forge2 : une copie du certificat honnête, augmentée d’une étape rdfs11 dont les prémisses lient ?b à deux valeurs différentes — (NamedPizza subClassOf Pizza) et (Food subClassOf Consumable) — concluant (NamedPizza subClassOf Consumable) ;
exécuter check_certificate sur cette forge avec la claim margherita/hasAllergen/milk et nommer la raison du rejet ;
expliquer en une phrase pourquoi aucune substitution ne peut sauver cette étape.
# Exemple guidé 2 — forge de la double liaison, rejet attendu.forge2 = copy.deepcopy(certificate)forge2["derivations"].append({"rule": "rdfs11","conclusion": [q("NamedPizza"), RDFS_SUBCLASS, q("Consumable")],"premises": [[q("NamedPizza"), RDFS_SUBCLASS, q("Pizza")], [q("Food"), RDFS_SUBCLASS, q("Consumable")]]})verdict_ex2 = check_certificate(forge2, claim_allergene, BUILTIN_RULES)print(f"verdict = {verdict_ex2['verdict'].upper()}")for p in verdict_ex2["problems"]:print(f" REJET — {p}")
Lecture — Exemple guidé 2 : zéro lecture, pas deux
Le rejet est INCONSISTENT_BINDING : la première prémisses lie ?b à Pizza, la seconde à Consumable — aucune substitution unique ne satisfait les deux patrons à la fois, donc l’étape n’est satisfaite par aucune lecture. C’est exactement la classe de défaut que la décision 0008 a fermée côté format : quand une liaison est ambiguë, ce n’est pas « deux lectures possibles », c’est zéro lecture — et le certificat doit être refusé, pas interprété.
Exercice 2 — La règle inconnue : faire entrer une règle par la fenêtre
Contexte : l’exemple guidé 2 a attaqué une étape (liaison incohérente). Une autre voie pour un forgeur : la référence de règle. La table de règles vit dans le certificat — le checker ne connaît que ce qu’elle contient.
Objectif :
forge3 : copie de certificate augmentée d’une étape citant la règle "rdfs5" — vérifiez d’abord son absence : sorted(certificate["rule_table"]). Prémisses (NamedPizza subClassOf Pizza) et (Pizza subClassOf Food) (toutes deux disponibles : l’une assertée, l’autre dérivée), conclusion (NamedPizza subClassOf Food). Vérifier la claim margherita/hasAllergen/milk : verdict et raison nommée ? Observez aussi claim_supported — et expliquez pourquoi la claim honnête reste « soutenue » dans un certificat pourtant rejeté ;
forge4 : forge3, mais avec "rdfs5"ajoutée à la table (patron de transitivité : ( ?a subClassOf ?b ) ; ( ?b subClassOf ?c ) => ( ?a subClassOf ?c )). Vérifier la claim (NamedPizza subClassOf Food) : verdict et rules_used — pourquoi le verdict n’est-il pasentailed, alors même qu’une dérivation honnête rdfs11 conclut le même triplet ?
toujours sur forge4, vérifier la claim (NamedPizza subClassOf Consumable) — une claim que l’étape forgée ne touche pas. Puis conclure en une phrase : une règle ajoutée au certificat peut-elle élever une claim vers entailed, ou seulement la dégrader ?
Indice : pour (a), que fait le checker quand d[“rule”] n’est pas une clé de rule_table ? Pour (b), regardez rules_reaching : la claim est conclue par DEUX étapes (l’honnête rdfs11 et la forgée rdfs5) — que fait l’union des règles utilisées ? - Etape 1 : forge3 = copy.deepcopy(certificate) ; forge3[“derivations”].append({…}) - Etape 2 : verdict sur claim_allergene — lire problems ET claim_supported - Etape 3 : forge4 = deepcopy + forge4[“rule_table”][“rdfs5”] = {…} ; verdict + rules_used - Etape 4 : claim non touchée sur forge4, puis formuler (c)
# Exercice 2 — à compléter# Etape 1 : forge3 (règle citée mais absente de la table)# Etape 2 : verdict sur claim_allergene — problems ET claim_supported# Etape 3 : forge4 (règle AUSSI ajoutée à la table) — verdict + rules_used# Etape 4 : claim non touchée sur forge4, réponse à (c)resultat_ex2 =None# TODO étudiant : pourquoi forge4 ne peut pas obtenir `entailed`print("Exercice 2 à compléter")
Exercice 2 à compléter
Exemple guidé 3 — Le slice minimal : ce qu’un retranchement préserve
Le README d’open-ontologies contient une ligne qui se relit deux fois : une retrieval slice à 99 % de couverture peut avoir perdu le seul triplet dont une réponse dépend — et une à 60 % peut préserver chaque claim qui compte. La couverture est un proxy ; la propriété, c’est la préservation d’entaillement, décidable ici, certificat à l’appui. Nous construisons ensemble le slice minimal — l’exercice 3 ci-dessous en jouera le miroir : non plus extraire le nécessaire, mais retirer l’essentiel et mesurer ce qui meurt.
Démarche guidée : écrire minimal_certificate(cert, claim) qui extrait du certificat complet le plus petit sous-certificat soutenant la claim :
marcher en arrière depuis la claim : quelles étapes (transitivement) la soutiennent, et quels faits assertés utilisent-elles ;
reconstruire un certificat ne contenant que ces étapes (dans l’ordre original) et ces faits ;
vérifier que le sous-certificat passe le checker sur la claim, et qu’il est minimal : retirer n’importe quelle étape restante fait échouer la claim.
# Exemple guidé 3 — slice minimal et test de minimalité.def minimal_certificate(cert, claim):# Marche arrière : étapes et faits assertés soutenant (transitivement) la claim. concl_to_idx = {}for i, d inenumerate(cert["derivations"]): concl_to_idx.setdefault(tuple(d["conclusion"]), []).append(i) needed_steps, needed_asserted =set(), set() asserted_set =set(tuple(t) for t in cert["asserted"]) stack, seen = [tuple(claim)], set()while stack: t = stack.pop()if t in seen:continue seen.add(t)if t in asserted_set: needed_asserted.add(t)continuefor i in concl_to_idx.get(t, []): needed_steps.add(i)for p in cert["derivations"][i]["premises"]: stack.append(tuple(p)) sous = {"format": cert["format"] +"/slice","rule_table": cert["rule_table"],"asserted": [list(t) for t in cert["asserted"] iftuple(t) in needed_asserted],"derivations": [cert["derivations"][i] for i insorted(needed_steps)], }return soussous_cert = minimal_certificate(certificate, claim_type)verdict_sous = check_certificate(sous_cert, claim_type, BUILTIN_RULES)print(f"Sous-certificat : {len(sous_cert['asserted'])} assertés, "f"{len(sous_cert['derivations'])} étapes (sur {len(certificate['derivations'])})")print(f"Verdict sur la claim : {verdict_sous['verdict']} "f"(règles : {verdict_sous['rules_used']})")# Minimalité : retirer chaque étape restante doit casser la claim.minimal =all(not check_certificate( {"format": sous_cert["format"], "rule_table": sous_cert["rule_table"],"asserted": sous_cert["asserted"],"derivations": [d for j, d inenumerate(sous_cert["derivations"]) if j != k]}, claim_type, BUILTIN_RULES)["claim_supported"]for k inrange(len(sous_cert["derivations"])))print(f"Minimalité (retrait de chaque étape casse la claim) : {minimal}")
Sous-certificat : 4 assertés, 3 étapes (sur 9)
Verdict sur la claim : entailed (règles : ['rdfs11', 'rdfs9'])
Minimalité (retrait de chaque étape casse la claim) : True
Lecture — Exemple guidé 3 : trois étapes sur neuf suffisent
Pour la claim margherita/type/Consumable, le slice complet tombe à 3 étapes sur 9 (et 4 faits assertés sur 9) : l’étape rdfs9 finale, l’étape rdfs9 qui établit margherita/type/Pizza, et l’étape rdfs11 qui établit Pizza/subClassOf/Consumable. Le retrait de n’importe laquelle casse la claim — c’est la définition opérationnelle d’un slice qui préserve, par opposition à un slice qui ne fait que couvrir. open-ontologies pousse cette idée jusqu’au théorème de localité (Cuenca Grau, Horrocks, Kazakov et Sattler, JAIR 31, 2008) pour ses modules d’ontologie — un théorème cité, pas machine-checké : voir la section 7.
Exercice 3 — L’amputation : validité globale du certificat vs support local d’une claim
Contexte : le slice minimal de l’exemple guidé 3 est constructif — il ne garde que le nécessaire. Le miroir destructif est tout aussi instructif : retirer une seule étape du certificat honnête et mesurer quelles claims perdent leur support. Et la sortie réserve une distinction que le checker code en dur : le verdict porte sur le certificat entier, claim_supported porte sur la claim seule — deux questions différentes.
Objectif : construire cert_ampute, copie de certificatesans l’étape rdfs11 qui conclut (Pizza subClassOf Consumable) — trouvez-la par son contenu, pas par son indice (les indices se décalent après retrait).
vérifier la claim margherita/type/Consumable (claim_type) sur cert_ampute : verdict, raisons nommées (PREMISE_NOT_AVAILABLE), claim_supported — combien d’étapes cassent, et que avaient-elles en commun ?
vérifier la claim margherita/hasAllergen/milk (claim_allergene) sur cert_ampute : verdict — et claim_supported ? Mesuré exactement : la claim garde son support (claim_supported: true) dans un certificat pourtant rejected. Expliquez pourquoi le checker est fail-closed : n’importe quel problème, même sans rapport avec la claim, rejette le fichier entier ;
calculer la couverture : len(cert_ampute["derivations"]) / len(certificate["derivations"]) — puis formuler en une phrase pourquoi un pourcentage de couverture ne prédit ni la mort ni la survie d’une claim (reliez à la retrieval slice du README citée en exemple guidé 3).
Indice : pour (a), listez les dérivations dont une prémisses est (Pizza, subClassOf, Consumable). Pour (b), relisez le régime du checker : un problème quelconque => verdict rejected pour le FICHIER ; claim_supported dit si la claim, elle, tenait sans l’étape retirée. - Etape 1 : cible = (q(“Pizza”), RDFS_SUBCLASS, q(“Consumable”)) ; cert_ampute = deepcopy de certificate sans l’étape qui la conclut - Etape 2 : check_certificate(cert_ampute, claim_type, BUILTIN_RULES) — verdict / problems / claim_supported - Etape 3 : check_certificate(cert_ampute, claim_allergene, BUILTIN_RULES) — verdict / claim_supported, expliquer le fail-closed - Etape 4 : couverture = len(cert_ampute[“derivations”]) / len(certificate[“derivations”]) ; réponse à (c)
# Exercice 3 — à compléter# Etape 1 : cert_ampute — retrait de l'étape concluant (Pizza, subClassOf, Consumable)# Etape 2 : claim_type sur cert_ampute — problems (combien d'étapes cassent ?)# Etape 3 : claim_allergene sur cert_ampute — verdict vs claim_supported (fail-closed)# Etape 4 : couverture et réponse à (c)resultat_ex3 =None# TODO étudiant : (couverture, pourquoi type meurt mais pas le support allergène)print("Exercice 3 à compléter")
Exercice 3 à compléter
7. Ce que le certificat NE prouve PAS
Le README d’open-ontologies consacre une section entière à ce qu’il ne prouve pas (« What is NOT proved ») et la place dans le README plutôt que dans un fichier que personne n’ouvre : « Every line above is worth less if this section is missing ». C’est une leçon de design en soi. Les limites ci-dessous sont celles qui portent le plus — vérifiées à la source au tag v1.4.0 :
Limite
Ce qu’elle signifie
Source
La provenance des assertions
le certificat dit « SI le graphe asserté est bien ce qu’il prétend, ALORS… ». Rien ne lie le graphe exporté au graphe raisonné : exporter A, raisonner sur B, et le checker accepte. L’issue #158 du dépôt (« certified input: the reasoner takes a value, not a store », décision 0010) documente le cas réalisé d’une réfutation valide prouvant l’inconsistance d’« une ontologie sur deux versions qui n’ont jamais coexisté » — the proof was correct; the graph was wrong
issue #158 (ouverte au tag v1.4.0)
Deux moteurs, un seul algorithme
le moteur Rust et le moteur Python pur (open-ontologies-lite) exécutent la même table de règles ; leur accord est une preuve contre l’erreur de transcription, quasi nulle contre une mélecture partagée d’une règle W3C. La jambe indépendante est le checker Lean
README v1.4.0, « What is in the box »
Le théorème de localité est cité, pas machine-checké
l’extraction de modules (onto_module_extract) repose sur le théorème de couverture de Cuenca Grau, Horrocks, Kazakov et Sattler (JAIR 31, 2008). Le rapport nomme le papier et jamais un théorème Lean, porte un champ guarantee_is_not_machine_checked, et un test (the_module_report_never_names_a_lean_theorem) l’exige
Le moteur Rust est presque entièrement non vérifié
sérialiseurs, parseurs, interner : tout ce qui est « à gauche » du certificat est testé par propriétés, borné par model-checking partiel — pas prouvé. Les théorèmes sont conditionnels
README v1.4.0, docs/trusted-computing-base.md
Les réponses négatives sont des opinions
une réfutation ne peut pas être rejouée dans core Lean : un « insatisfiable » est un témoignage d’oracle, pas un certificat. Le vocabulaire distingue systématiquement le mesuré du prouvé (décision 0006)
README v1.4.0
Appliqué à notre jouet : le checker de la section 4 vérifie une procédure, sans théorème ; il ne sait rien de la provenance des 9 faits assertés ; et si nous écrivions une seconde implémentation du moteur en copiant la première, leur accord ne prouverait rien — c’est le checker qui doit être indépendant, pas le moteur duplicata.
8. L’honnêteté documentaire comme discipline — le commit 55abe97
Le 5 septembre 2026, le dépôt open-ontologies livre un commit au titre volontairement banal : « Correct the claims the docs made about the engine ». Son message (lu intégralement à la source) mérite l’étude :
A sweep of ten claims found 131 copies across 37 files. The documentation had drifted from the code far enough that a reader checking any of it would have found the repository contradicting itself.
Dix affirmations, 131 occurrences, 37 fichiers, +483/−150 lignes. Les corrections sont de la matière première pour un cours sur les claims :
Claim avant
Vérité mesurée
Forme du défaut
« 109 tools »… ou « 70+ », « 50+ », « 103 », « 43 » selon les fichiers
109 au moment du sweep
quatre fichiers, quatre nombres
« the reasoner is SHOIQ »
SHIQ — pas de nominaux, owl:oneOf jamais parsé
fragment survendu
« 0 disagreements with HermiT »
« 0 unsound rejections » — 23 des 78 884 paires restent au palier résiduel
le « sans désaccord » masquait une incomplétude
le quickstart promet un modèle d’embeddings téléchargé par init
réservé aux builds avec feature embeddings
promesse hors build publié
Et la discipline va jusqu’aux tests : no_stale_tool_count_survives_anywhere vérifie que les comptes des docs sont dérivés du code, pas retapés à la main — un compteur qui dérive fait échouer la CI.
La leçon est vivante, et ce notebook s’y est plié lui-même. Le chiffre « pizza ≈ 1 345 axiomes » circulait dans le corps de l’issue d’origine de ce notebook : introuvable dans le dépôt au tag — nous ne l’avons pas répété, et la section 6 ne cite que des mesures (1 944 triplets, 99 classes, 218 individus sur data/pizza.owl ; 258 dérivations). De même, le README du tag v1.4.0 annonce « 114 tools » alors que le sweep de septembre en comptait 109 : le compte évolue vite, on cite tag + date, jamais un nombre nu. C’est la même règle que ce dépôt applique à ses propres notebooks (valeurs dérivées des sorties, jamais retapées) — deux projets indépendants, la même conclusion : un claim non mesuré est une dette.
9. Avec une preuve, sans une preuve — la table fil rouge, définitive
Question
Sans preuve (SW-13 : owlrl, HermiT…)
Avec certificat — jouet (sections 2-5)
Avec certificat — open-ontologies v1.4.0 (section 6)
Pourquoi croire la conclusion ?
« le raisonneur l’a dit »
9 étapes relues, prémisses ground
258 étapes émises, prémisses ground
Qui peut vérifier ?
qui ré-exécute le moteur
tout lecteur du fichier JSON
tout lecteur des TSV — checker Lean prouvé sound (OOCert.certificate_sound)
Conclusion forgée ?
indétectable
rejetée 5 fois sur 5 (forges A-D + E)
rejetée (forge E : CONCLUSION_MISMATCH)
Règle métier ?
même statut qu’un fait
entailed_under_supplied_rules ≠ entailed
même distinction, testée par la CI
Le « non » (insatisfiable) ?
opinion
hors scope du jouet
opinion d’oracle — dite comme telle
Coût de vérification ?
ré-exécuter le raisonnement
relire le fichier
relire le fichier (+ théorème déjà payé)
Cross-links — où ce notebook se branche dans le dépôt
SW-13-Python-Reasoners — le gap que ce notebook comble : benchmark de raisonneurs sans preuve transportable ;
#16751 / #16741 (vericoding vs vibe coding, Epic Tegmark) — le pont désigné : prouver les programmes générés par LLM côté code, prouver les inférences d’une base de connaissances côté données. open-ontologies incarne la boucle complète : un LLM écrit l’ontologie (plugin Claude/MCP, ~120 outils onto_*), le moteur certifie, Lean prouve le certificat — « l’agent écrit, la machine prouve » ;
Z3-Linq2Z3 — open-ontologies utilise Z3 et cvc5 comme oracles différentiels ; nos notebooks SMT sont le prérequis naturel du geste « croiser plusieurs vérificateurs sur le même objet » ;
SW-15 / Tweety — les justifications minimales (prémisses qui soutiennent une conclusion, exemple guidé 3) résonnent avec les warrants de l’argumentation formelle : notre slice minimal est l’analogue épistémique d’un argument sans attaque ;
#5721 (prior art) — l’ingénierie ontologique Argumentum → CoursIA (SKOS, AIF.owl) : l’ontologie AIF de SW-15 et la validation certifiée de SW-16 sont les deux moitiés d’un même programme ;
Lean — la série pousse l’idée à son terme : ici le checker est décrit, là-bas il est prouvé.
Conclusion — le gap comblé, et ce qui reste
Ce que vous emportez :
Une conclusion de raisonneur sans preuve transportable est un acte de confiance ; le certificat en fait un fait vérifiable par un tiers qui ne fait pas confiance au moteur ;
Émettre la preuve coûte peu : un forward chaining naïf qui enregistre règle + conclusion + prémisses — sans beaucoup plus de code que la clôture owlrl de SW-13 ;
Vérifier coûte encore moins : relire chaque étape sous une seule substitution, exiger la disponibilité ordonnée des prémisses — et refuser nommément (5 familles de rejets démontrées) ;
Le verdict est honnête par construction : entailed vs entailed_under_supplied_rules, l’oracle distingué du certificat, les limites écrites (provenance #158, moteurs jumeaux, théorème cité non machine-checké).
Ce qui reste ouvert — et c’est le programme : la provenance des assertions (issue #158 ouverte au tag : le certificat le plus juste ne prouve rien si le graphe asserté ment) ; la réfutation certifiée ; et pour ce dépôt, la déclinaison Lean du checker jouet — un compagnon à kernel Lean qui compilerait horn_certificate_sound sur notre mini-table de règles serait le prolongement naturel (la série Lean en a tous les outils).
Ressources : open-ontologies au tag v1.4.0 (moteur + lean/OOCert + docs/decisions/) ; Rovai, Open Ontologies: Tool-Augmented Ontology Engineering with Stable Matching Alignment, arXiv:2605.09184 (2026) ; Cuenca Grau, Horrocks, Kazakov et Sattler, Modular Reuse of Ontologies: Theory and Practice, JAIR 31, 2008 ; Necula, Proof-Carrying Code, POPL 1997.