Sortenlogik

aus Wikipedia, der freien Enzyklopädie
Wechseln zu: Navigation, Suche

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. Die Sortenlogik stellt für diese Prädikate eine Spezialbehandlung der eben erwähnten Form zur Verfügung. Da viele Deduktionschritte hierbei wegen der Sortenunverträglichkeit nicht in Betracht gezogen werden, verringert sich der Suchaufwand nach einem Beweis beträchtlich, wie die Praxis zeigt.