Termersetzung: Grundlagen

Zusammenfassung

Im vorigen Kapitel haben wir begonnen, die Gleichheit als ausgezeichnetes Prädikatensymbol innerhalb des Prädikatenkalküls zu studieren: zunächst in klassischer Weise mit den Gleichheitsaxiomen und normaler Resolution, dann mit Paramodulation. Jetzt wollen wir einen Schritt weiter gehen und unseren Kalkül so weit spezialisieren, daß die Gleichheit das einzige Prädikatensymbol ist. Tatsächlich liegen bei vielen Anwendungen Formelmengen vor, die ausschließlich aus Gleichungen bestehen. Hier ergeben sich Querbezüge zu verschiedenen anderen Gebieten der Informatik, etwa zur Funktionalen Programmierung, wo - abweichend von zustandsorientierten imperativen Sprachkonzepten - einzelne Ausdrücke durch Regelanwendungen in andere umgeformt werden, oder zur Algebraischen Spezifikation, wo mit Gleichungen Abstrakte Datentypen definiert werden, siehe Ehrig & Mahr [EM85].