Die vorliegende Dissertation beinhaltet eine umfassende Untersuchung der Entscheidbarkeit und Komplexität der Probleme, die sich durch eine statische Analyse von monadischem Datalog auf endlichen gefärbten Bäumen stellen. Statische Analyse bedeutet hierbei Anfrageoptimierung ohne Blick auf konkrete Instanzen, aber mit Rücksicht auf deren zugrunde liegende Struktur. Im Kern beinhaltet dies die Lösung der drei folgenden Probleme: das Leerheitsproblem (die Frage, ob eine Anfrage auf jeder Instanz ein leeres Ergebnis liefert), das Äquivalenzproblem (die Frage, ob zwei Anfragen auf jeder Instanz das gleiche Ergebnis liefern) und das Query-Containment-Problem (die Frage, ob das Ergebnis der einen Anfrage auf jeder Datenbank im Ergebnis der anderen Anfrage enthalten ist). Von Interesse ist dabei, ob die Fragen für eine gegebene Anfragesprache entscheidbar sind und wenn ja, welche Komplexität ihnen innewohnt. Wir betrachten diese Probleme für monadisches Datalog auf unterschiedlichen Repräsentationen für endliche gefärbte Bäume. Hierbei unterscheiden wir zwischen ungeordneten und geordneten Bäumen, welche die Achsen child bzw. firstchild und nextsibling und deren Erweiterung um die descendant-Achse nutzen. Außerdem unterscheiden wir Alphabete mit und ohne Rang. Monadisches Datalog ist eine Anfragesprache, die in Abhängigkeit vom gewählten Schema die Ausdrucksstärke der monadischen Logik zweiter Stufe (MSO) erreicht und dennoch effizient ausgewertet werden kann. Wir zeigen, dass unter in der Datenbanktheorie üblichen Mengensemantik die drei genannten Probleme für alle Schemata ohne descendant-Achse EXPTIME-vollständig sind und lösbar in 2EXPTIME, falls die descendant-Achse involviert ist. Eine passende untere Schranke wird für fast alle Schemata gezeigt. Unter Multimengensemantik lassen sich die obigen Ergebnisse für das Leerheitsproblem übertragen, während das Query-Containment-Problem für alle betrachteten Schemata unentscheidbar ist. / This thesis provides a comprehensive investigation into the decidability and complexity of the fundamental problems entailed by static analysis of monadic datalog on finite labeled trees. Static analysis is used for optimizing queries without considering concrete database instances but exploiting information about the represented structure. Static analysis relies on three basic decision problems. First, the emptiness problem, whose task is to decide whether a query returns the empty result on every database. Second, the equivalence problem asking if the result of two given queries always coincides on every database. And finally, the query containment problem where it is to decide whether on every database a given query produces a subset of the results of a second given query. We are interested in finding out whether these problems are decidable and, if so, what their complexity is. We consider the aforementioned problems for monadic datalog on different representations of finite labeled trees. We distinguish unordered and ordered trees which use the axis child, as well as the axes firstchild and nextsibling, respectively. An extension of the schemas by the descendant-axis is also considered. Furthermore, we distinguish ranked and unranked labeling alphabets. Depending on the schema, the query language monadic datalog can reach the expressive power of monadic second order logic but remains efficiently evaluable. Under set semantics, we show EXPTIME-completness for all used schemas where the descendant-axis is omitted. If the descendant-axis is involved, we present an algorithm that solves the problem within 2-fold exponential time. A matching lower bound is proven for virtually all schemas. Finally, we prove that the complexity of the emptiness problem of monadic datalog on finite trees under bag semantics is the same as under set semantics. Furthermore, we show that the query containment problem of monadic datalog under bag semantics is undecidable in general.

Query equivalence is a fundamental problem within database theory. The correctness of all forms of logical query rewriting—join minimization, view flattening, rewriting over materialized views, various semantic optimizations that exploit schema dependencies, federated query processing and other forms of data integration—requires proving that the final executed query is equivalent to the original user query. Hence, advances in the theory of query equivalence enable advances in query processing and optimization. In this thesis we address the problem of deciding query equivalence between conjunctive SQL queries containing aggregation operators that may be nested. Our focus is on understanding the interaction between nested aggregation operators and the other parts of the query body, and so we model aggregation functions simply as abstract collection constructors. Hence, the precise language that we study is a conjunctive algebraic language that constructs complex objects from databases of flat relations. Using an encoding of complex objects as flat relations, we reduce the query equivalence problem for this algebraic language to deciding equivalence between relational encodings output by traditional conjunctive queries (not containing aggregation). This encoding-equivalence cleanly unifies and generalizes previous results for deciding equivalence of conjunctive queries evaluated under various processing semantics. As part of our study of aggregation operators that can construct empty sub-collections—so-called “scalar” aggregation—we consider query equivalence for conjunctive queries extended with a left outer join operator, a very practical class of queries for which the general equivalence problem has never before been analyzed. Although we do not completely solve the equivalence problem for queries with outer joins or with scalar aggregation, we do propose useful sufficient conditions that generalize previously known results for restricted classes of queries. Overall, this thesis offers new insight into the fundamental principles governing the behaviour of nested aggregation.

Query equivalence is a fundamental problem within database theory. The correctness of all forms of logical query rewriting—join minimization, view flattening, rewriting over materialized views, various semantic optimizations that exploit schema dependencies, federated query processing and other forms of data integration—requires proving that the final executed query is equivalent to the original user query. Hence, advances in the theory of query equivalence enable advances in query processing and optimization. In this thesis we address the problem of deciding query equivalence between conjunctive SQL queries containing aggregation operators that may be nested. Our focus is on understanding the interaction between nested aggregation operators and the other parts of the query body, and so we model aggregation functions simply as abstract collection constructors. Hence, the precise language that we study is a conjunctive algebraic language that constructs complex objects from databases of flat relations. Using an encoding of complex objects as flat relations, we reduce the query equivalence problem for this algebraic language to deciding equivalence between relational encodings output by traditional conjunctive queries (not containing aggregation). This encoding-equivalence cleanly unifies and generalizes previous results for deciding equivalence of conjunctive queries evaluated under various processing semantics. As part of our study of aggregation operators that can construct empty sub-collections—so-called “scalar” aggregation—we consider query equivalence for conjunctive queries extended with a left outer join operator, a very practical class of queries for which the general equivalence problem has never before been analyzed. Although we do not completely solve the equivalence problem for queries with outer joins or with scalar aggregation, we do propose useful sufficient conditions that generalize previously known results for restricted classes of queries. Overall, this thesis offers new insight into the fundamental principles governing the behaviour of nested aggregation.

Answer set programming (ASP) is a declarative approach to solving search problems. Logic programming constitutes the foundation of ASP. ASP is not a proof-theoretical approach where you get solutions by answer substitutions. Instead, the problem is represented by a logic program in such a way that models of the program according to the answer set semantics correspond to solutions of the problem. Answer set solvers (Smodels, Cmodels, Clasp, and Dlv) are used for finding answer sets of a given program. Although users can write programs with variables for convenience, current answer set solvers work on ground logic programs where there are no variables. The grounding step of ASP generates a propositional instance of a logic program with variables. It may generate a huge propositional instance and make the search process of answer set solvers more difficult. Model generation theorem provers (Paradox, Darwin, and FM-Darwin) have the capability of producing a model when the first-order input theory is satisfiable. This work proposes the use of model generation theorem provers as computational engines for ASP. The main motivation is to eliminate the grounding step of ASP completely or to perform it more intelligently using the model generation system. Additionally, regardless of grounding, model generation systems may display better performance than the current solvers. The proposed method can be seen as lifting SAT-based ASP, where SAT solvers are used to compute answer sets, to the first-order level for tight programs. A completion procedure which transforms a logic program to formulas of first-order logic is utilized. Besides completion, other transformations which are necessary for forming a firstorder theory suitable for model generation theorem provers are investigated. A system called Completor is implemented for handling all the necessary transformations. The empirical results demonstrate that the use of Completor and the theorem provers together can be an eective way of computing answer sets. Especially, the run time results of Paradox in the experiments has showed that using Completor and Paradox together is favorable compared to answer set solvers. This advantage has been more clearly observed for programs with large propositional instances, since grounding can be a bottleneck for such programs.