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