Analyse von regelbasierten Constraintlösern by Slim Abdennadher Institut für Informatik, Ludwig-Maximilians-Universität München, Germany Um Constraintlöser in einer höheren Sprache schnell und ausreichend effizient zu spezifizieren und implementieren, wurde in der ersten Hälfte der 90er Jahre eine spezielle regelbasierte Sprache, "Constraint Handling Rules" (CHR), entwickelt. CHR kann in eine beliebige herkömmliche Programmiersprache als Bibliothek eingebettet werden. Die derzeit wichtigsten Implementierungen von CHR-Bibliotheken gibt es in Eclipse und Sicstus Prolog, zwei der in der Forschung am meisten benutzten Prolog-Systeme. In dieser Arbeit werden einerseits einige Eigenschaten von CHR untersucht, andererseits einige mittels CHR implementierten Anwendungen vorgestellt. Eine essentielle, jedoch bei einer Regelsprache wie CHR nicht offensichtliche Eigenschaft eines Constraintlösers ist die Konfluenz. Sie garantiert, daß dasselbe Ergebnis berechnet wird, unabhängig davon, in welcher Reihenfolge die Constraints eintreffen und in welcher Reihenfolge die CHR-Regeln darauf angewandt werden, um sie abzuarbeiten. In dieser Arbeit wird ein notwendiges, hinreichendes und entscheidbares syntaktisches Kriterium für die Konfluenz von terminierenden CHR-Programmen entwickelt. Dieses Kriterium ergab sich durch Erweiterung des Begriffes der kritischen Paare aus dem Bereich der Termersetzungssysteme. Eine unmittelbare Übertragung der Ergebnisse über Konfluenz von Termersetzungssystemen auf CHR-Programme ist nicht möglich. Ein weiteres Ergebnis der Arbeit ist ein Verfahren, das in vielen Fällen ein terminierendes nicht-konfluentes CHR-Programm zu einem terminierenden konfluenten transformiert, das äquivalent zum ursprünglichen ist. Dieses Verfahren ist eine Variante der Vervollständigung von Knuth und Bendix. Anschließend werden einige Anwendungen vorgestellt, die zeigen, daß die Constraint-Sprache CHR sich zur einfachen Programmierung beziehungsweise "rapid prototyping" eignet, ohne daß die Effizienz beeinträchtigt wird.