benutzerdefinierte Funktionen,
definiert durch Gleichungen (Ersetzungsregeln)
Rechnen = Normalform bestimmen
benutzerdefinierte Relationen (Prädikate),
definiert durch Schlußregeln (Implikationen).
Rechnen = Schlußfolgerung (Widerspruch) ableiten