Next: Dynamische GLB-Berechnung Up: Sortenbedingungen Previous: Bedingungen an die

Bedingungen an die Instantiierung der Sorten

Da Sorten hier als logische Sprachelemente implementiert werden sollen, ist es n"otig,

zu fordern, d.h. jede Sorte beschreibt mindestens ein Individuum . Es gibt auch Ans"atze [Wei94] in denen Sorten nicht-strikt sein m"ussen. Dabei wird die sortierte Unifikation um einen Checker erweitert, der testet, ob das Ergebnis einer Unifikation zweier Sorten die leere Sorte ist.

Weiter sollte die Instantiierung die

erf"ullen, d.h. der intensionale Schnitt zweier Sorten (GLB) ist gleich dem extensionalen Schnitt, das ist der Schnitt "uber der Menge von Instanzen, die durch die Sorte repr"asentiert werden. Je nach Instantiierung der Sorten kann die Kommutativit"at von Unifikationskonjunktionen verletzt werden.

Der intensionale Schnitt in Abbildung der Sorten $a und $b liefert die Sorte $c. Betrachtet man den extensionalen Schnitt von $a und $b, erh"alt man die Menge {2,3}, die der Instantiierung {3}der Sorte $c widerspricht. Benutzt man den benutzerdefinierten GLB $c dennoch f"alschlicherweise als GLB, so liefern folgende Konjunktionen von Literalen eine Kommutativit"atsverletzung bei einer Links-Rechts-Abarbeitung:

Man beachte, da"s durch die Voraussetzung der Vollst"andigkeit auch die Bedingung der Eindeutigkeit gew"ahrleistet ist, da der extensionale Schnitt eindeutig ist.

All diese Voraussetzungen sind bei einer sauberen Modellierung automatisch erf"ullt, k"onnten aber bei inkrementellem Aufbau der Taxonomie entstehen. Unbedingt erf"ullt sein m"ussen aus logischer und semantischer Sicht die Restriktionen Striktheit und Zyklenfreiheit. In Spezialf"allen k"onnte man eventuell auf Vollst"andigkeit und Eindeutigkeit verzichten. Es ist vorstellbar, da"s der definierte GLB aus semantischen Gr"unden nicht unbedingt gleich dem extensionalen Schnitt sein mu"s, nur sollten sich Benutzer und Entwickler "uber die Folgen im klaren sein. Ist die Eindeutigkeit verletzt, es gibt also ,,mehrere GLB's``, wird bei der hier vorgestellten Implementierung, der zuerst gefundene GLB zur"uckgeliefert. Welcher GLB zuerst gefunden wird, ist jedoch von der Reihenfolge der taxonomiebeschreibenden Regeln oder entsprechenden subsumes-Fakten abh"angig.



Next: Dynamische GLB-Berechnung Up: Sortenbedingungen Previous: Bedingungen an die


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