Repository navigation
Tranche A — laboratoire propositionnel Tweety↔Lean : validité, preuve, contre-modèle (Part of #15066) #15521
Description
Activity
[CLAIMED] lane myia-po-2026:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/propositional_lean/PropositionalTweetyLab.lean, MyIA.AI.Notebooks/SymbolicAI/Tweety/propositional_lab.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/propositional_lean/PropositionalTweetyLab_en.lean -- Tranche A EPIC #15066 : laboratoire propositionnel Tweety<->Lean (validite, preuve, contre-modele). Conditionne sur verdict favorable #15520 ou workaround documente. Grain: DEEP/lean -- lane myia-po-2026:CoursIA-2 -- prev: MED/test #15492.
[INFO] candidate-delivered — #15521 (Tranche A) est LIVREE ; aucun reprise n'est requise
Constat firsthand (lane
myia-po-2024:CoursIA, 2026-09-13T12:4xZ) apres le tirage du picker, qui a servi cette issue comme grain neuf.La livraison existe, et elle est sur
mainAncre Mesure PR #15692 feat(notebook,#15066): Tweety-5e -- laboratoire propositionnel Tweety/Lean (tranche A)Tag Grain: DEEP/notebook-lean — lane myia-po-2024:CoursIA — prev: DEEP/research-code #15645Etat MERGED 2026-09-12T11:30:04Z (squash 1c9a4ac8fa)Artefact MyIA.AI.Notebooks/SymbolicAI/Tweety/Tweety-5e-Propositional-Lab-Lean.ipynb— blobf6625f40surorigin/mainLe claim
[CLAIMED] myia-po-2026:CoursIA-2(2026-09-11T02:11:18Z) est perime a 58,5 h —check_lane_claim.py 15521 --lane myia-po-2024:CoursIArendSTALE_CLAIM … reprise autoriseeetblocking_lanes: []. La reprise est donc autorisee mais inutile : les trois chemins revendiques (PropositionalTweetyLab.lean,propositional_lab.ipynb,…_en.lean) n'existent sur aucun disque — le travail est passe par un autre nom de fichier, ce que l'organe signale parWARN: glob sans correspondancesur les trois.Acceptance, confrontee au contenu reel du notebook (pas au body)
Mesure sur
git show origin/main:…Tweety-5e-Propositional-Lab-Lean.ipynb: 30 cellules, 10 code, 10 executees, 10 avec sorties, 0 erreur.Critere Verdict Memes formules sur les deux moteurs, serialisation commune montree OK — section 1 : trois formules-temoins ( SYL+ deux autres) serialisees a la fois en syntaxe Tweety ((a => b) => …) et en arbre Lean (🡒)≥1 theoreme ET ≥1 contre-modele cote Lean ; controle negatif satisfiable-non-valide OK — section 4 (certificat 1, theoreme prouve) et section 5 (certificat 2, contre-modele transporte de Tweety vers Lean), sur les 8 mondes du fragment {a,b,c}Claims metatheoriques citant le module FFL exact OK — import Foundation.Propositional.Formula.Basic, kernel natif sur FFL, pin verifie en celluleDependance au pin, verdict #15520 favorable OK — #15520 CLOSED le 2026-09-11, verdict CONSUMER_PINNENotebook execute, ≥3 exercices, stubs C.1 OK — 3 exercices, stubs print("Exercice a completer …"), aucunraise NotImplementedErrorREADME serie mis a jour NON — residu reel, voir ci-dessous Le seul residu : l'entree README (et le blocage qui la retient)
#15692a change 1 seul fichier (changed_files=1). Le README de la serie ne connait donc pasTweety-5e: mesure surorigin/main,grep -nE "5[bcde]" …/Tweety/README.mdliste 5b, 5c, 5d — jamais 5e — et les comptes qui en derivent sont perimes (l.32 « soit 14 notebooks » pour la colonne Python ; l.742 le breakdown « Lean companion (5b, 5d) | 2 » ; l.410-411 l'arbre de structure). Le notebook est donc invisible depuis le README de sa propre serie.Ce residu n'est pas prenable par une lane a cet instant : la PR #15942 (
chore(catalog): scheduled auto-regenerate, longue duree, rafraichie chaque jour) est OUVERTE et toucheMyIA.AI.Notebooks/SymbolicAI/Tweety/README.md. Editer ce chemin maintenant produirait la collision de chemin que L898 interdit — l'organePR-PATH-COLLISIONla signale deja sur #15942 elle-meme.Geste attendu du coordinateur : sequencer l'entree README 5e (audit §E fichier-entier : table l.162-164, table resume l.205-206, arbre l.410-411, breakdowns l.742/749, comptes re-mesures) apres le merge de #15942 — ou l'attacher a la passe qui suit.
La fermeture de #15521 appartient au coordinateur/adjoint : une lane worker ne ferme pas d'issue. Elle est complete a l'exception du residu ci-dessus.
— lane
myia-po-2024:CoursIA, 2026-09-13[CLAIMED] lane myia-po-2024:CoursIA -- paths: MyIA.AI.Notebooks/SymbolicAI/Tweety/README.md -- residu d'acceptance de la Tranche A : entree Tweety-5e dans le README de serie + comptes re-mesures (audit fichier-entier §E). La livraison #15692 a change 1 seul fichier, le README de la serie ignore donc 5e. 2026-09-13T13:1xZ
- added a commit that references this issue
on Sep 14, 2026 FERMEE — verification firsthand contre
origin/main@0dcc80c1fb7b748646b500672ef4df1873ba8013.Tranche A livree par #15692 (
1c9a4ac8fa) et #15980 (1b3b7594c1), toutes deux MERGED.Tweety-5e-Propositional-Lab-Lean.ipynbest sur main (30 cellules, 10 code executees), avec la serialisation commune Tweety/Lean, le theoreme prouve (certificat 1) et le contre-modele (certificat 2), l'import FFL exactFoundation.Propositional.Formula.Basicsur pin verifie, et 3 exercices a stubs conformes C.1 (print("Exercice a completer"), aucunraise NotImplementedError). Le README de serie est reconcilie sur six emplacements, changelog compris.
Part of #15066 — Tranche A de l'EPIC Formalized Formal Logic. Bloquée par le verdict du pilote #15520.
Objectif
Companion transversal de Tweety-2 / Lean-3 : laboratoire propositionnel — validité, preuve et contre-modèle. Une même formule et un même petit modèle traversent l'exécution Tweety et les objets certifiés Lean, avec contrôles croisés falsifiables.
Contenu (verbatim de la Tranche A, EPIC #15066)
Foundation/Propositional;satisfiable,valid,provable;Vrai raisonneur Tweety + kernel Lean natif — aucune réimplémentation jouet (SOTA, sota-not-workaround).
Acceptance