Filtern
Erscheinungsjahr
- 2012 (25) (entfernen)
Dokumenttyp
Sprache
- Englisch (25) (entfernen)
Schlagworte
- Petri-Netze (2)
- probability propagation nets (2)
- 101companies (1)
- API Analysis (1)
- API Migratiom (1)
- Archivierung (1)
- Automatisches Beweisverfahren (1)
- Beschreibungslogik (1)
- Cloud Computing (1)
- Computerspiel (1)
- Content Management (1)
- Core Ontology on Multimedia (COMM) (1)
- Criteria Matrix (1)
- Design Pattern (1)
- E-Hyper Tableau (1)
- E-KRHyper (1)
- ECMS 2012 (1)
- Enterprise 2.0 (1)
- Enterprise Information Management (1)
- Entwurfsmuster (1)
- European Conference on Modelling and Simulation (1)
- GPGPU (1)
- Germany (1)
- Hypertableaux (1)
- Java <Programmiersprache> (1)
- Linked Open Data (1)
- Logik (1)
- Maschinelles Sehen (1)
- Natural Feature Tracking (1)
- ODRL (1)
- Ontology alignment (1)
- Petrinetz (1)
- Proceedings (1)
- Prozedurale Synthese (1)
- Registratur (1)
- Schema Information (1)
- Schlussfolgern (1)
- Softwareentwicklung (1)
- Softwarewartung (1)
- Taxonomy (1)
- Tokens (1)
- Tool Evaluation (1)
- University (1)
- Web Analytics (1)
- Web Analytics Framework (1)
- Web Mining (1)
- Web-application framework (1)
- Web-programming technologies (1)
- Wikipedia (1)
- archiving (1)
- description logic (1)
- design thinking (1)
- deutsche Hochschulen (1)
- distinct object identifiers (1)
- entrepreneurial design thinking (1)
- entrepreneurial thinking (1)
- entrepreneurship education (1)
- faceted search (1)
- hypertableaux (1)
- metadata formats (1)
- metadata standards (1)
- mobile devices (1)
- multimedia metadata (1)
- procedural content generation (1)
- shiq (1)
- social media data (1)
- teams (1)
- tool-integration (1)
- unique name assumption (1)
- video games (1)
- virtual goods (1)
Institut
- Fachbereich 4 (25) (entfernen)
In einigen Bereichen des automatischen Theorembeweisens benötigt man das Wissen, dass Konstanten paarweise ungleich sind. Um dieses zu erreichen, fügt man Fakten, die dieses Wissen explizit angeben, zu den Wissensbasen hinzu. Wenn man diese Eigenschaft für viele Konstanten definieren muss, wird die Klauselmenge der Wissensbasen schnell sehr umfangreich und wegen der vielen - eigentlich irrelevanten - Ungleichheiten kann man den Blick auf das eigentlich formalisierte Problem verlieren. Da die Größe der Wissensbasis in vielen Fällen Einfluss auf die Geschwindigkeit hat, ist es auch aus diesem Grund sinnvoll, die Anzahl dieser Fakten gering zu halten. Die unique name assumption erlaubt auf die Einführung der Ungleichheits-Fakten zu verzichten, da sie festlegt, dass zwei Konstanten genau dann gleich sind, wenn ihre Interpretationen identisch sind. Auf diesem Wege lässt sich das Aufblähen von Wissensbasen mit Ungleichheits-Fakten verhinde. In dieser Arbeit wird der E-Hyper-Tableau-Kalkül erweitert um die unique name assumption nutzen zu können. Der in dieser Arbeit entwickelte Kalkül ist vollständig und korrekt, was durch formale Beweise in dieser Arbeit belegt wird. Um zu zeigen, dass die native Behandlung von Ungleichheiten dem Einführen von Ungleichheits-Fakten überlegen ist, wird der Kalkül in den Theorembeweiser E-KRHyper implementieren. Der Theorembeweiser E-KRHyper ist ein etabliertes System und basiert in seiner ursprünglichen Version auf dem E-Hyper-Tableau. Mit systematischen Tests wird dann gezeigt, dass die entwickelte Implementierung des erweiterten Kalküls nie schlechter ist, als der original E-KRHyper, diesen aber in einigen Fällen in der Ausführungsgeschwindigkeit deutlich übertrifft.