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ädika...