Sortenlogik

Sortenlogik ordnet jedem Term in einer Formel eine Klasse zu, die man in diesem Zusammenhang Sorte nennt, und die Unifikation nur dann zulässt, wenn beide Terme von der gleichen Sorte sind.

Aus dem Blickwinkel der Prädikatenlogik (ohne Sorten) sind solche Sorten einstellige Prädikate (wie z. B. Vogel). Die Sortenlogik stellt für diese Prädikate eine Spezialbehandlung der eben erwähnten Form zur Verfügung. Da viele Deduktionsschritte hierbei wegen der Sortenunverträglichkeit überhaupt nicht in Betracht gezogen werden, verringert sich der Suchaufwand nach einem Beweis beträchtlich, wie die Praxis zeigt.