Eine Variable in einer prädikatenlogischen Formel kann innerhalb eines Beweises mit jedem Term substituiert werden. Entscheidend ist allein die Unifizierbarkeit. Dahinter verbirgt sich eine der großen Flexibilitäten bezüglich der Wissensrepräsentation aus der Sicht des menschlichen Benutzers. Ein ungeschicktes Vorgehen bei der Abarbeitung kann hier jedoch andererseits einen großen unnötigen Berechnungsaufwand verursachen. Tatsächlich ist man auf dieses Phänomen erst in jüngerer Zeit gestoßen, als sich herausstellte, daß vermeintlich leistungsfähige Deduktionssysteme an relativ einfachen Problemen genau aus dem gerade geschilderten Grunde scheiterten. Dies hat zu einer Verfeinerung der Systeme geführt. Dabei ist man zwei verschiedene Wege gegangen.
Der eine Weg besteht darin, daß man jedem Term in einer Formel eine Klasse
zuordnet, die man in diesem Zusammenhang Sorte nennt, und
die Unifikation nur dann zuläßt, wenn beide Terme von der gleichen
Sorte sind. Aus dem Blickwinkel der Prädikatenlogik (ohne Sorten) sind
solche Sorten einstellige Prädikate (wie zB. Vogel). Die Sortenlogik
[Wal87] stellt für diese Prädikate, die in Formeln ohne Sorten
in der Form 
oder
auftreten würden, 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.
Sorten haben daher in jüngerer Zeit eine große Popularität erworben. Als Typen waren sie in Programmiersprachen ohnehin schon lange im Gebrauch. Aber auch in Wissensrepräsentationssprachen (wie KRL, wo sie mit ``Kategorien'' bezeichnet werden) bilden sie meist einen wichtigen Sprachaspekt, den wir in Abschnitt 2.6 bei den Vererbungssystemen im einzelnen studiert haben. Von daher wissen wir, daß die Sorten untereinander in Beziehungen stehen, wobei es sich im Spezialfall der hierarchischen Taxonomien um partielle Ordnungen handelt. In der Sortenterminologie spricht man in diesem Spezialfall von einer Sortenlogik mit Ordnung (engl. order-sorted logic) [BHP+92].
Der andere von den beiden oben genannten Wegen besteht in einer Kontrollstruktur für Beweissysteme, die sich an der Syntax der Formel orientiert und dabei Besonderheiten wie die stereotype Deduktionsstruktur bei Sortendefinitionen der oben illustrierten Form erkennt und zur Effizienzsteigerung (in einer kostenmäßig vernachlässigbaren Vorverarbeitung) ausnützt. Dieser Zugang, der in [Bib87b, BLS87] genauer beschrieben ist, resultiert in der Hauptverarbeitung in einem mit der Sortenlogik vergleichbaren Suchverhalten (vgl. auch [LSBB92]). Es ist allgemeiner als die Sortenlogik, da die genannten Besonderheiten auch bei mehrstelligen Prädikaten auftreten, reduziert den Suchraum also auch da, wo die Sortenlogik überhaupt nicht greift. Schließlich erspart es dem Benutzer, sich mit dem Ballast der Sorten auseinanderzusetzen, wenn er dies nicht will. Wegen des letzteren Arguments sind jüngst Systeme entwickelt worden, die die Sortierung automatisch besorgen. De facto realisieren sie nichts anderes als diesen soeben beschriebenen syntaktischen Zugang. Die Autoren beurteilt all diese Argumente als eindeutig für diesen zweiten Weg sprechend.
Christoph Quix, Thomas List, René Soiron