Tableauxbeweiser entstammen der künstlichen Intelligenz. Mit ihrer Hilfe kann man maschinell Schlussfolgerungen aus Wissensbasen ziehen, die im Repräsentationsformalismus der Beschreibungslogiken (engl. Description Logic, DL) vorliegen. Im Rahmen eines Praktikums wurde im WS 2005/06 eine mobile Variante eines solchen Tableaux Reasoners entwickelt, die - zumindest theoretisch - auf jedem Java-fähigen Endgerät lauffähig ist, ganz speziell auch auf Mobiltelefonen.

 

Für die Formulierung von Wissenszusammenhängen (-> Ontologien) gibt es bereits einige verbreitete Programme. Zu den bekannteren Vertretern gehört das Programm Protégé der Universität Stanford. Über eine TCP-Verbindung können Anfragen zu einer Wissensbasis an einen Reasoner gesendet werden, der diese beantwortet und das Ergebnis wieder zurückliefert. Dafür wird das DIG-Interface (DL Implementation Group, XML-Format) verwendet. Da Handys nicht direkt per TCP angesprochen werden können (außer über das teure WAP), und Protégé keine Bluetooth-Unterstützung bietet, findet die Kommunikation über ein kleines Proxyprogramm statt, das auf dem PC läuft und als Mittelsmann fungiert. Es leitet die per TCP ein- und ausgehenden Daten an die Bluetoothverbindung weiter und umgekehrt. Beantwortet werden die Anfragen auf dem Mobiltelefon, das seine Ergebnisse wiederum im DIG-Format zurückliefert.

 

Der eigentliche Reasoner wurde mit Hilfe des Java Wireless Toolkits (WTK) von Sun entwickelt. Dabei handelt es sich mehr oder weniger um eine abgespeckte Java-API für mobile Geräte. Der beigepackte Emulator ermöglicht das Testen auf PCs, Bluetooth-Unterstützung ist seit der Version WTK 2.2 BETA mit an Bord. Für das Parsen der DIG-Dateien ist in unserem Reasoner der XML-Parser kxml2 zuständig, dessen jar-Archiv mit 40KB angenehm klein ausfällt. Wesentlich komplizierter als die mobile Seite war anfangs die Programmierung des Desktop-Programms, da das JDK von Sun keine Bluetooth-Unterstützung mitbringt. Zwar gibt es verschiedene Implemetierungen des Bluetooth-Stacks von Zweitanbietern, diese sind jedoch entweder sehr teuer oder bieten nicht den gewünschten Funktionsumfang. Bewährt hat sich letztlich die Verwendung des freien BlueCove, das allerdings bislang nur Windows XP SP2 unterstützt. Dennoch konnten wir leider nicht alle Probleme lösen. Unser Programm hat sich auf dem Sun Emulator anders verhalten als auf dem Handy und auch die Bluetooth-Verbindung hatte bis zuletzt einige Kinderkrankheiten.

 

Warum das Ganze? Im Internet finden sich diverse Vorschläge, wozu ein mobiler Tableauxbeweiser nützlich sein könnte. Hier sei mal exemplarisch ein Szenario genannt: Stellen wir uns ein Kino vor, das sein Kinoprogramm per Bluetooth an die Handys seiner Besucher versendet. Der Tableaux Reasoner, der auf den Mobiltelefonen installiert ist, könnte nun aus den bisher besuchten Filmen ableiten, welche Filme für den Handybesitzer von Interesse sein könnten und entsprechende Vorschläge machen. Beispielsweise könnte er eine Vorliebe für Actionfilme ausmachen und den neuen James Bond Streifen empfehlen und eventuell gleich einen freien Termin im Kalender ermitteln. Wie nützlich das ist, muss natürlich jeder selbst wissen. ;-)

 

Ein schöner Abschluss: auf dem Description Logic Workshop 2006 wurde unser Projekt in Form eines Posters/Papers präsentiert. :-)