Skip to content

fix(notebooks,#17550): Z3-12-Real-Arithmetic-Python — 1 cellule markdown nettoyee du doublage de newlines #18237

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
myia-ai-01 merged 2 commits into from
Sep 29, 2026
Merged

fix(notebooks,#17550): Z3-12-Real-Arithmetic-Python — 1 cellule markdown nettoyee du doublage de newlines #18237

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2bdbc83
fix(notebooks,#17550): Z3-12-Real-Arithmetic-Python — 1 cellule markd…
claude Sep 28, 2026
52c8e1c
Merge branch 'main' into fix/17550-z312-real-arith-newlines
jsboige Sep 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 1 addition & 5 deletions MyIA.AI.Notebooks/SymbolicAI/SMT/Z3-API/Z3-12-Real-Arithmetic-Python.ipynb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.)"
]
},
Expand Down Expand Up @@ -562,4 +558,4 @@
},
"nbformat": 4,
"nbformat_minor": 5
}
}
Loading