- Signatur:
- Funktionssymbole beliebig
- Relationssymbol nur =
mathend000#
- Universum: Terme
(d.h. Leibniz-Axiom für =
mathend000#)
- Formel: Konjunktion von Gleichungen
(zwischen Termen mit Variablen)
Anwendungen: Verarbeitung symbolischer Ausdrücke
- logische Programmierung (Prolog)
- Typprüfung, Typinferenz
(für polymorphe Funktionen)
2014-03-31
