Generalisierung: Algorithmen und Anwendungen

Generalisierung ist ein Prozess zur Gewinnung allgemeinerer Objekte aus konkreten. Es ist ein wesentliches Konzept im induktiven Schliessen. In seiner einfachsten Form ist eine Generalisierung zweier logischer Terme ein Term, aus welchem die beiden ursprünglichen Terme durch Variablensubstitution gewonnen werden können. Unter all diesen Generalisierungen sind die interessantesten jene, die nicht spezieller gemacht werden können: die least general generalizations. Die Berechnung von least general generalizations nennt man Anti-Unification. Es ist eine duale Prozedur zur Unifikation, bei der die allgemeinsten gemeinsamen Instanzen von gegebenen Termen berechnet werden. Aktuelle Forschung über Anti-Unifikation ist durchsetzt von praktisch orientierten Themen, was nicht verwunderlich ist, denn die Berechnung von Generalisierungen in ihren verschiedenen Formen ist ein wichtiger Bestandteil in vielen Anwendungen im Automatischen Schliessen, Informationsgewinnung, Lernen, Datenkompression, Softwareentwicklung und -Analyse und so weiter. In diesem Projekt werden wir uns mit den Schwierigkeiten befassen, die sich für die Generaliserung aus neuen Anwendungsfeldern ergeben. Einige davon machen es nötig, Generalisierungsprobleme in völlig neuen Theorien zu untersuchen. Einige andere lassen sich wohl durch die Verbesserung von bekannten Algorithmen behandlen. Es ist bekannt, dass in vielen Anwendungen die übliche Anti- Unifikation erster Ordnung zu schwach ist. Wir beschäftigen uns mit der Entwicklung von Generalisierungsalgorithmen für Gleichungs-Theorien und Theorien höherer Ordnung (auch in Bezug auf Ähnlichkeitsrelationen und für komprimierte Terme), und deren Analyse, Untersuchung effizienter Spezialfälle, freie open source Implementierungen, und Anwendungen.

Generalisierung ist ein Prozess zur Gewinnung allgemeinerer Objekte aus konkreten. Es ist ein wesentliches Konzept im induktiven Schliessen. In seiner einfachsten Form ist eine Generalisierung zweier logischer Terme ein Term, aus welchem die beiden ursprünglichen Terme durch Variablensubstitution gewonnen werden können. Unter all diesen Generalisierungen sind die interessantesten jene, die nicht spezieller gemacht werden können: die least general generalizations. Die Berechnung von least general generalizations nennt man Anti-Unification. Es ist eine duale Prozedur zur Unifikation, bei der die allgemeinsten gemeinsamen Instanzen von gegebenen Termen berechnet werden. Aktuelle Forschung über Anti-Unifikation ist durchsetzt von praktisch orientierten Themen, was nicht verwunderlich ist, denn die Berechnung von Generalisierungen in ihren verschiedenen Formen ist ein wichtiger Bestandteil in vielen Anwendungen im Automatischen Schliessen, Informationsgewinnung, Lernen, Datenkompression, Softwareentwicklung und -Analyse und so weiter. In diesem Projekt haben wir uns mit den Herausforderungen befasst, die sich für die Generalisierung aus neuen Anwendungsfeldern ergeben. Wir entwickelten neue Generalisierungsalgorithmen für für Gleichungs-Theorien und Theorien höherer Ordnung (auch in Bezug auf Näherelationen und für komprimierte Terme), analysierten sie, untersuchten effiziente Sonderfälle, stellten eine kostenlose Open-Source-Implementierung bereit und diskutierten Anwendungen. Das Projekt hat wichtige Beiträge zur Weiterentwicklung des Standes der Technik von Generalisierungsalgorithmen geleistet und neue Forschungsprobleme aufgeworfen, die in Zukunft untersucht werden sollen.