...Anwendermodells)
Formal soll als Behauptungswissen das gesamte Wissen, das weder die Taxonomie beschreibt noch Sorten instantiiert, bezeichnet werden.

...k;;onnte
Diese Arbeitsteilung wurde z.B. in COLAB [BHHM93] an der TAXON-CONTAX-Schnittstelle zur Constraintpropagierung "uber hierarisch strukturierten Dom"anen erprobt.

...Deklaration
Sorten werden hier nur implizit deklariert, d.h. wenn der Bezeichner einer Sorte erstmals auftritt, ist aus dem Text des Bezeichners bzw. aus der Stelle des Programms, an der er auftritt, eindeutig erkennbar, wie die fehlende Deklaration lauten m"u"ste.

...subsumes
subsumes ist ein bin"ares Pr"adikat der Pr"adikatenlogik 2. Stufe "uber un"are Pr"adikate 1. Stufe

...wird
subsumes-Notation und Hornregel-Notation sind gerichtet in dem Sinn, da"s erkennbar ist, was Ober- und was Untersorte ist.

...bindet
is unifiziert i.A. seine linke und rechte Seite.

...beschr;;ankt
Da die Individuen mittels un"arer Fakten den Sorten zugeordnet werden, k"onnen die Sorten, f"ur die Individuen definiert werden extensional, benutzt werden. Allerdings werden dann nur die Individuen aufgez"ahlt, die (direkt) f"ur diese Sorte definiert wurden, da subsumes(P, Q) anders als P(X) :- Q(X) nicht f"ur (indirekte) Folgerungen ausgenutzt wird.

...,,Sortenwissen``
Sortenwissen definiert die Sortenhierarchie und die Instantiierung der darin enthaltenen Sorten.

...Unifikation
Da der GLB zweier disjunkter Sorten nicht existiert, scheitert eine entsprechende Unifikation.

...Sorten
Letztlich kann man nur endliche Sorten beschreiben, da Sorten extensional definiert werden.

...Dom;;anen
Endliche Dom"anen sind verwandt mit endlichen Mengen und Aufz"ahlungstypen.

...erlauben
Wenn man endliche Sorten als benannte Dom"anen versteht, mu"s folglich auch die Unifikation endlicher Sorten mit Exklusionen erlaubt sein (endliche Dom"anen sind mit Exklusionen unifizierbar [Bol94]).

...werden
Im Rahmen dieser Arbeit wurden zwar nur endliche Sorten implementiert, doch die Erweiterung zu unendlichen Sorten wird theoretisch ber"ucksichtigt.

...
Zyklenfreiheit wird in der Literatur auch oft als Antisymmetrie bezeichnet.

...
Schlaufen werden in der Literatur auch oft durch die Eigenschaft der Reflexsivit"at beschrieben.

...Sorten
Allerdings kann man durch Mitprotokollieren der bereits betrachteten Sorten bei dieser Berechnung Endlosschleifen erkennen. Will man diesen zus"atzlichen Aufwand verhindern, mu"s man eine zyklenfreie Taxonomie fordern.

...Vertr;;aglichkeit
Die Frage, welche Gesichtspunkte vertr"aglich sind, ist eng mit der Frage, welche Pr"adikate "uberhaupt zu einer Sorte erhoben werden d"urfen, verbunden.

...
Vollst"andigkeit wird hier i.S.v. ,,Intensional-Extensionale Schnittgleichheit`` verwendet.

...Individuum
Denn sonst k"onnte man das extralogische Pr"adikat var aus PROLOG realisieren.var(X) :- X is $a. wobei die Sorte $a nicht-strikt (unbewohnt) ist. Falls die Variable X an irgendeinen (nicht variablen) Wert gebunden ist (inklusive $a), wird ein FAIL ausgel"ost; ist die Dereferenzierung von X frei, ist die Regel erfolgreich.

...Individuum
Erlaubt man nicht-strikte Sorten, kann nicht garantiert werden, da"s das Herbrand-Universum nicht leer ist. Das f"uhrt zu einem Modellierungsfehler [CGH94].

...GLB
Im Falle einer nicht-eindeutigen Taxonomie wird die Liste ,,aller GLB's`` zur"uckgegeben.

...clause-Builtin
Das clause-Pr"adikat ist ein second-order Pr"adikat. Hier: clause(P(X) :- Q(X).) = t P(X) :- Q(X) oder '(hn (_p_x) (_q_x))) in der betrachteten Partition existiert

...Sortenlisten
Sortenliste: (sortenname (SUBSUMES ..) (INDIVIDUALS ..) (SUBSUMES* ..) (INDIVIDUALS* ..))

...GLB-Berechnung
Ebenso ist der Test, ob eine Konstante als Individuum einer Sorte definiert wurde, statisch.

...(sortbase)
Dabei ist die gew"ahlte Notation, also Hornregeln oder Subsumes-Fakten, unwichtig.

...werden
Die momentane Implementierung erlaubt keine "Anderung in der compilierten Sortbase-Datenstruktur. Dies ist durch intelligente Einf"uge-/ L"oschfunktion, die die interne vorcompilierte Datenstruktur ver"andern, erreichbar. Dazu sind die Listen SUBSUMES und INDIVIDUALS n"otig; deshalb werden sie schon jetzt in der Sortbase-Datenstruktur mitgef"uhrt.

...VEGA
Das VEGA-Projekt behandelt die Validierung und Exploration von Wissensbanken durch globale Analyse

Harold Boley & Victoria Hall (hall@dfki.uni-kl.de)