Reasoning with forest logic programs

Answer Set Programming (ASP) ist ein beliebter, regelbasierter Formalismus zur Beschreibung und Lösung von kombinatorischen Suchproblemen. Open Answer Set Programming (OASP) erweitert Answer Set Programming um eine Semantik mit offenen Domänen: Programme erhalten eine Interpretation in beliebigen Dömanen, die anonyme Individuen enthalten kann, d.h. Individuen, die nicht explizit im Programm aufscheinen. Dies ermöglicht es mittels OASP generisches Wissen zu formulieren. Gleichzeitig erbt OASP von ASP die nicht-monotone Behandlung der Negation unter der stabilen Modell-Semantik (Stable Model Semantics). OASP verbindet auf seine Art zwei wichtige Paradigmen der Wissensrepräsentation: die klassische Prädikatenlogik erster Stufe (First-Order Logic, FOL) und die Welt der nicht-monotonen Regeln. Im allgemeinen Fall ist OASP unentscheidbar. Um Entscheidbarkeit zu erreichen wurden deshalb verschiedene Fragmente von OASP durch deshalb syntaktische Einschränkungen der Form der Regeln definiert. Beispiele solcher Fragmente sind Conceptual Logic Programs (CoLPs) - ein Fragment, das die Verwendung von Konstanten verbietet und die Tree-Modell Eigenschaft erfüllt -, und Forest Logic Programs (FoLPs) - ein Fragment mit der Forest-Modell Eigenschaft. CoLPs können Schließen (engl. Reasoning) in der Beschreibungslogik (engl. Description Logic) SHQ simulieren und es wurde durch eine Reduktion auf two-way alternating tree automata gezeigt, dass sie entscheidbar sind. FoLPs hingegen können Reasoning in der Beschreibungslogik SHOQ simulieren, aber es war vor dieser Arbeit nicht bekannt, ob sie entscheidbar sind oder nicht. Entscheidbarkeit war vorher nur für Fragmente von azyklischen und lokalen FOLPs bewiesen, in denen die Verwendung von Rekursion sehr stark eingeschränkt ist. Deswegen ist der Reasoning-Support für CoLPs und FoLPs ziemlich begrenzt. Die Forest-Modell Eigenschaft von FOLPs eröffnet die Möglichkeit, sie mit tableau-basierten Methoden zu untersuchen, die Modelle mit Forest Form erzeugen. Im Gegensatz zur Reduktion auf Automaten, sind zielorientierte Prozeduren wie Tableau-Algorithmen nicht worst-case optimal, aber sie eignen sich für Optimierungen und verhalten sich in der Praxis gut. Daher ist das Ziel der Arbeit, tableau-basierte Algorithmen für das Reasoning mit FoLPs zu entwickeln. Die Wahl von FoLPs erfolgte, weil sie ein sehr ausdrucksstarkes Fragment von OASP sind, das auch CoLPs umfasst. Eine der größten Herausforderungen bei der Entwicklung von Tableau-Algorithmen für FoLPs besteht darin, für jedes Atom im konstruierten Modell sicher zu stellen, dass es "well-supported" ist, d.h. dass es eine Begründung für das Atom im Modell gibt, die weder zirkulär noch unendlich ist. Die Erweiterung des Standard Blocking, wie es von Tableau Algorithmen angewandt wird, um die Überprüfung von Well-Supportedness ist aber nicht ausreichend, um die Termination des Verfahrens zu garantieren. Deswegen stützen sich unsere Algorithmen stark auf Techniken mit denen für FoLPs die Finite-Modell Eigenschaft erreichtwerden kann; diese werden dann in Laufzeit-Endbedingungen umgewandelt. Basierend auf zwei solche Techniken entwickeln wir Algorithmen für die Überprüfung der Erfüllbarkeit (engl. Satisfiability) für unäre Prädikate bezüglich FoLPs, die im schlechtesten Fall nichtdeterministisch doppelt exponentielle bzw. nichtdeterministisch einfach exponentielle Laufzeit haben. Während die zweite Klasse von Algorithmen ein besseres Laufzeitverhalten im schlechtesten Fall aufweist, erfordert sie ausführliche Aufzeichnungen (engl. Bookkeeping). Wir identifizieren ein neues Fragment von FoLPs, simple Forest Logic Programs, das azyklische FoLPs verallgemeinert und für die man einen unkomplizierten nicht-deterministischen Algorithmus entwickeln kann. Die oben erwähnten Algorithmen zeigen, dass Satisfiability-Testen von unären Prädikaten in FoLPs in nichtdeterministische einfach exponentieller Zeit entschieden werden kann. Aufgrund der Tatsache, dass FoLPs Reasoning in der Description Logic SHOQ simulieren können, wissen wir, dass Reasoning in FolPs EXPTIME hart ist. Auf der Suche nach worst-case optimalen Algorithmen untersuchen wir die Determinisierung der oben erwähnten Algorithmen mit Hilfe von AND/OR Datenstrukturen. Wir erhalten zwei worst-case optimale Algorithmen für das Reasoning mit Fragmenten von CoLPs und einfachen FoLPs.