Definition
Ein rekursiver Projektions‑und‑Lifting‑Algorithmus, der den reellen n‑dimensionalen Raum in endlich viele zylindrisch angeordnete Zellen aufteilt (Zellen, deren Projektionen auf niedrigere Dimensionen Zellen der Zerlegung sind), so dass eine gegebene endliche Menge reeller Polynome auf jeder Zelle ein unverändertes Vorzeichen besitzt und somit Entscheidungsverfahren für Vorzeichen‑ und Quantorfragen ermöglicht.
Prinzip
Prinzip
Polynommengen schrittweise um jeweils eine Variable projektieren, um Projektionspolynome zu berechnen, die Randbedingungen erfassen, dann durch Isolierung reeller Nullstellen und Aufbau höherdimensionaler Zellen aufwärts heben, sodass jede Zelle vorzeicheninvariant für die ursprünglichen Polynome ist; die zylindrische Eigenschaft garantiert kompatibles Stapeln der Zellen über Dimensionen.
Demonstration
Demonstration
Zur Entscheidung von ∃x p(x,y)>0 projiziere p in x, bestimme Diskriminanten und Resultanten in y, finde kritische y‑Werte, die die reelle Achse partitionieren, und hebe dann in jedem Intervall, indem man Probenwerte in x und Vorzeichenmuster berechnet, um zu prüfen, ob für dieses y‑Intervall ein x mit p>0 existiert.
Fehlanwendung
Fehlanwendung
CAD indiscriminately auf Probleme mit vielen Variablen oder hohen Graden anzuwenden führt zu unpraktikabler Berechnung, da die Projektion viele Polynome erzeugt; CAD auf komplexe (nichtreelle) Probleme anzuwenden oder Numerik der Nullstellenisolation zu ignorieren kann zu falschen Zelldeskriptionen führen.
Konsequenz
Konsequenz
CAD liefert ein vollständiges Entscheidungsverfahren für Formeln erster Ordnung über wirklich abgeschlossenen Körpern: es erzeugt explizite Zellzerlegungen zur Auflösung von Quantoren und Vorzeichenbedingungen und kann Stützpunkte sowie exakte Beschreibungen semialgebraischer Mengen liefern, allerdings bei potenziell hoher Komplexität.
Umkehrung
Umkehrung
Anstelle eines vollständigen CAD kann man partielle CAD, virtuelle Substitution oder numerische Abtastung und Intervallmethoden nutzen; dies ersetzt eine vollständige vorzeicheninvariante zylindrische Zerlegung durch günstigere, möglicherweise unvollständige Alternativen.
Abgrenzung
Abgrenzung
Gilt für Polynome mit reellen Koeffizienten und für reale Quantorenelimination; behandelt nicht direkt transzendente Funktionen oder komplexe Variablenanfragen und skaliert ohne Heuristiken oder problemspezifische Reduktionen nicht effizient bei vielen Variablen und hohen Graden.
Semantische Spannung
Semantische Spannung
CAD garantiert Vorzeicheninvarianz und Entscheidbarkeit für reale Quantorenprobleme, leidet jedoch an worst‑case doppelt exponentieller Komplexität; Gröbnerbasen oder numerische Solver sind für manche algebraische oder approximative Aufgaben effizienter, bieten aber nicht die allgemeine Quantorenbehandlung von CAD.
Synthese
Synthese
Zylindrische Algebraische Zerlegung ist ein Projektions‑und‑Lifting‑Schema, das eine endliche vorzeicheninvariante Partition des reellen Raums in zylindrisch kompatible Zellen erzeugt; es wandelt Quantor‑ und Vorzeichenfragen über Polynome in kombinatorische Prüfungen auf Zellen und Stützpunkten um und tauscht allgemeine Entscheidbarkeit gegen hohen Rechenaufwand ein.