| Summary: | We outline a novel technique that maps the satisfiability problems of
second-order logics, in particular WSnS (weak monadic second-order
logic with n successors), S1S (monadic second-order logic with one
successor), and of μ-calculus, to the problem of query evaluation
of Complex-value Datalog queries. In this dissertation, we propose
techniques that use database evaluation and optimization techniques
for automata-based decision procedures for the above logics. We show
how the use of advanced implementation techniques for Deductive
databases and for Logic Programs, in particular the use of tabling,
yields a considerable improvement in performance over more traditional
approaches. We also explore various optimizations of the proposed
technique, in particular we consider variants of tabling and goal
reordering. We then show that the decision problem for S1S can be
mapped to the problem of query evaluation of
Complex-value Datalog queries.
We explore optimizations that
can be applied to various types of formulas. Last, we propose
analogous techniques that allow us to approach μ-calculus
satisfiability problem in an incremental fashion and without the need
for re-computation. In addition, we outline a top-down evaluation
technique to drive our incremental procedure and propose heuristics
that guide the problem partitioning to reduce the size of the problems
that need to be solved.
|
|---|
