Es sei eine Menge an
-Ausdrücken
(über einem
Symbolalphabet
),
die
abgeschlossen unter Ableitungen
ist. Dann definiert man auf der Menge aller
-Terme
eine
Äquivalenzrelation
durch
-
Es sei die Menge der Termklassen
(also die Menge der Äquivalenzklassen zu dieser Äquivalenzrelation).
Auf definiert man für jedes -stellige
Relationssymbol
eine -stellige
Relation
durch
-
und für jedes -stellige
Funktionssymbol
eine -stellige
Funktion
durch
-
Konstanten werden als
-
interpretiert.