Ziel der vorliegenden Arbeit ist die Entwicklung eines modular aufgebauten Erfüllbarkeitstesters für verschiedene unimodale und eine polymodale Beschreibungslogik, die zur Repräsentation von agentenabhängig modelliertem terminologischen Wissen genutzt werden kann. Es werden dazu Tableaukalküle eingeführt, und deren Implementationen vorgestellt. Die Tableaukalküle bearbeiten Beschreibungslogik- und Modallogikanteile getrennt, dieser Trennung folgt dann auch der Aufbau des Testers. Zur Bearbeitung der Beschreibungslogikanteile wird das System FaCT benutzt, welches als Modul in den Erfüllbarkeitstester integriert wird. Eine notwendige Vorverarbeitungsstufe wird von einem weiteren Modul realisiert. Für die Performance des gesamten modularen Systems spielt die interne Kommunikation eine entscheidene Rolle. Deshalb ist eine optimierte Variante der Kommunikation zwischen FaCT und dem Gesamtsystem entwickelt worden. Während des Tests verschiedener Formeln eines Benchmarks konnte das hier entwickelte modulare System im Vergleich mit anderen Systemen akzeptable Leistungen erbringen.
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:16626 |
| Date | 26 October 2017 |
| Creators | Hofmann, Thomas |
| Contributors | Universität Leipzig |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | German |
| Detected Language | German |
| Type | info:eu-repo/semantics/acceptedVersion, doc-type:masterThesis, info:eu-repo/semantics/masterThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
| Relation | urn:nbn:de:bsz:15-qucosa2-163403, qucosa:16340 |
Page generated in 0.0026 seconds