Symbolisches Rechnen für Identitäten linearer Operatoren

Viele Prozesse in Naturwissenschaft und Technik können mittels linearer Systeme von sogenannten Funktionalgleichungen modelliert werden. Um solche Systeme zu bearbeiten und zu analysieren, führt man Berechnungen mit den entsprechen Matrizen und linearen Operatoren durch. Die Eigenschaften von Systemen und Operatoren werden durch Identitäten beschrieben. Anstatt mit konkreten Matrizen und Operatoren arbeitet man beim Symbolischen Rechnen mit Symbolen, welche die mathematischen Objekte darstellen. Das übergeordnete Ziel des Projekts Symbolisches Rechnen für Identitäten linearer Operatoren ist es mittels Computern solche formale Rechnungen mit Operatoren und Klassen von Systemen über das derzeit Mögliche hinaus zu automatisieren. Insbesondere geht es dabei um Symbolische Methoden und Computeralgebra für das Beweisen und Finden von Identitäten linearer Operatoren sowie für das Lösen von Operatorgleichungen. Im Rahmen des Projekts entwickeln wir Methoden zur Untersuchung von Klassen dynamischer Systeme aus der Technik und deren Regelung. Diese Systeme, wie auch deren Transformationen, werden meist mittels Differential-, Verzögerungs- und Integraloperatoren modelliert. Um mit solchen Operatoren zu rechnen erarbeiten wir eindeutige Darstellungen für sie. Diese Normalformen verwenden wir dann um Operatoridentitäten mittels Computeralgebrasoftware, die im Laufe des Projekts entwickelt wird, automatisiert zu beweisen wie auch zu entdecken. Sind Input und Output der Operatoren bzw. Matrizen von unterschiedlicher Dimension so können diese nicht in beliebiger Weise addiert oder verknüpft werden. Dies schränkt Rechnungen mit Operatoren und Matrizen ein. Im Rahmen des Projekts erarbeiten wir neue symbolische Methoden um mit diesen Einschränkungen umzugehen. Das Prinzip besteht darin, zunächst symbolisch ohne Einschränkungen zu rechnen und dann das Ergebnis zu rechtfertigen und zwar unabhängig davon wie dieses erlangt wurde.

Viele Prozesse in Naturwissenschaft und Technik lassen sich durch lineare Systeme von sogenannten Funktionalgleichungen modellieren. Zur Bearbeitung und Analyse solcher Systeme werden Berechnungen mit den entsprechenden Matrizen und linearen Operatoren durchgeführt. Viele wichtige Eigenschaften von Systemen und Operatoren lassen sich durch Gleichungen beschreiben. In der Computeralgebra arbeitet man dabei mit Symbolen, die die mathematischen Objekte und die dazugehörigen Gleichungen darstellen. Das Ziel des Projekts "Symbolisches Rechnen für Identitäten linearer Operatoren" war es, mittels Computern diese formalen Rechnungen mit Operatoren und Klassen von Systemen über das bisher Mögliche hinaus zu automatisieren. Das automatische Beweisen und Finden von Operatorgleichungen befindet sich dabei an der Schnittstelle zwischen Computeralgebra und Künstlicher Intelligenz. Ein zentrales Ergebnis des Projekts ist ein allgemeines Framework für das automatisierte Beweisen von Aussagen über Identitäten linearer Operatoren unter Verwendung von Berechnungen mit nichtkommutativen Polynomen. In den Publikationen werden alle Aspekte dieses Ansatzes behandelt, einschließlich der logischen und algebraischen Grundlagen, neuer Algorithmen, heuristischer Überlegungen, effizienter Implementierungen, frei verfügbarer Softwarepakete und umfassender Fallstudien. Wir konnten dabei zahlreiche klassische Resultate über verallgemeinerte Inverse sowie Ergebnisse aus aktuellen Forschungsarbeiten in wenigen Sekunden mit unserer Software beweisen. Gemeinsam mit unseren Kooperationspartnern haben wir mithilfe von Computerunterstützung auch neue Resultate über sogenannte Moore-Penrose-Inverse gefunden und allgemein bewiesen. Ein wichtiger Aspekt unseres Ansatzes ist, dass zu jeder wahren Aussage über Identitäten von Operatoren ein Zertifikat berechnet wird, das unabhängig von unserer Software leicht verifiziert werden kann. In diesem Sinne ist die entwickelte Methode theoretisch vollständig. Dank neuer Algorithmen, heuristischer Überlegungen und einer effizienten Implementierung kann die Software auch in der Praxis Beweise für aktuelle Forschungsfragen zu linearen Operatoren liefern. Identitäten von linearen Operatoren aus der Analysis, wie Ableitung, Integration und Auswertungen, waren ein weiterer Forschungsschwerpunkt des Projekts. Wir beschreiben alle algebraischen Gleichungen, die diese Operatoren erfüllen, in einer aktuellen Publikation in einem führenden Mathematikjournal. Insbesondere zeigen wir, dass zwölf Rewrite-Regeln ausreichen, um jeden Ausdruck auf eine eindeutige Normalform zu vereinfachen. Für den computerunterstützten Beweis der Vollständigkeit dieser Regeln haben wir einen neuen theoretischen Ansatz und eine eigene Software entwickelt. Mithilfe dieser Rewrite-Regeln können einerseits klassische Identitäten aus der Analysis und Resultate für Systeme von linearen Differentialgleichungen rein algebraisch bewiesen werden. Andererseits ermöglicht der algebraische Ansatz auch Verallgemeinerungen der Taylorformel sowie Shuffle-Relationen für verschachtelte Integrale auf Funktionen mit Singularitäten, wie sie beispielsweise in der theoretischen Physik bei Berechnungen für Quantenfeldtheorien auftreten.