Reasoning with forest logic programs

Abstract

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.

Answer Set Programming (ASP) is a popular rule-based formalism for describing and solving combinatorial search problems. Open Answer Set Programming (OASP) extends ASP with an open domain semantics: programs are interpreted with respect to arbitrary domains which might contain anonymous individuals, i.e. individuals which do not occur explicitly in the program. In the general case, OASP is undecidable. With the purpose of achieving decidability, several fragments have been devised by means of syntactical restrictions on the shape of rules. Some such fragments are Conceptual Logic Programs (CoLPs), a fragment which has the tree model property, and Forest Logic Programs (FoLPs), a generalization of CoLPs with constants. At the beginning of this work, the reasoning support for CoLPs and FoLPs was rather limited and it was not known whether FoLPs are decidable. In this thesis we describe tableau-based algorithms for reasoning with FoLPs and sub-fragments. We first devise algorithms for satisfiability checking of unary predicates with respect to FoLPs which run in the worst-case in non-deterministic double and non-deterministic single exponential time, respectively. One of the main challenges when designing such algorithms is ensuring that every atom in a constructed model is well-supported, i.e. there is a reason for the presence of the atom in the model and this reason is not circular or infinite. This leads to rather sophisticated bookkeeping. As such, we identify a new fragment of FoLPs, called simple Forest Logic Programs, for which a straightforward non-deterministic tableau algorithm can be devised. In a quest to obtain worst-case optimal algorithms, we investigate the determinisation of the above-mentioned algorithms by means of AND/OR data structures. We obtain two worst-case optimal algorithms to reason with the fragments of CoLPs and simple FoLPs, respectively.