From 2bdbc83ced8258091ca9350ec4b5959efcb1b1ce Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Mon, 28 Sep 2026 15:43:54 +0200 Subject: [PATCH] =?UTF-8?q?fix(notebooks,#17550):=20Z3-12-Real-Arithmetic-?= =?UTF-8?q?Python=20=E2=80=94=201=20cellule=20markdown=20nettoyee=20du=20d?= =?UTF-8?q?oublage=20de=20newlines?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Haiku 4.5 (1M context) --- .../SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb index fd8fad6927..c25673409c 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb @@ -6,13 +6,9 @@ "metadata": {}, "source": [ "← [11 - Coloration de graphe](Z3-11-Graph-Coloring-Python.ipynb) | [README Z3-Python](README.md)\n", - "\n", "# 12. Arithmetique reelle : raisonner sur les irrationnels exacts\n", - "\n", "Jusqu'ici nous avons raisonne sur des **entiers** (coloration de graphe, cryptarithmes, ordonnancement). Z3 sait aussi raisonner sur les **reels** via la théorie `Real` (SMT-LIB `Reals`). C'est une capacite profondement différente : les solutions peuvent etre **rationnelles exactes** (pas d'arrondi flottant), des **irrationnels algebriques** (racine carree de 2 representee comme racine d'un polynome, pas comme 1.4142...), et l'absence de solution peut etre **prouvee** (`unsat`) sur le corps des reels tout entier.\n", - "\n", "Ce notebook explore les trois postures : arithmetique lineaire (solution rationnelle exacte), non-lineaire (irrationnel algebrique), et preuve d'impossibilite sur R. Aucun `float`, aucun `sqrt()` approche : tout est symbolique.\n", - "\n", "> Port pyz3 du notebook C# [`16_RealArithmetic.ipynb`](../Z3-Linq2Z3/16_RealArithmetic.ipynb). EPIC #1206, Prong B. (La section B7 Rational du C#, spécifique au DSL Z3.Linq, n'est pas portee.)" ] }, @@ -562,4 +558,4 @@ }, "nbformat": 4, "nbformat_minor": 5 -} +} \ No newline at end of file