By Tobias Kaminski,
Due to current trends in distributed systems and information integration, there is an increasing need for accessing external information sources from within knowledge representation formalisms such as answer set programming (ASP). For instance, it might be necessary to integrate information derived from a (possibly remote) description logics (DL)-ontology into the computation of an answer set. If the derivation in the ontology is relative to information in the ASP-part, a bidirectional exchange between a DL-reasoner and an ASP-solver is required.
This kind of interaction is not provided by ordinary ASP, and pre-computing all possible derivations from the ontology and adding them to the answer set program is often not feasible. Motivated by this, the HEX-formalism has been developed, where external sources can be referenced in a program, and are evaluated during solving. The approach is related to SAT modulo theories (SMT), but the focus is more on techniques for evaluating general external sources represented by arbitrary computations, i.e. it enables an API-like approach such that a user can define plugins without expert knowledge on solver construction. HEX-programs are very expressive since the bidirectional exchange of information between a logic program and external sources encompasses the formalization of non-monotonic and recursive aggregates. Consequently, HEX is suited for a wide range of applications, but also requires sophisticated evaluation algorithms to deal with the complexity that goes along with the high expressiveness. For this reason, this thesis work aims at the design and implementation of novel integrated evaluation techniques with the overall goal to improve the efficiency of the formalism in general, as well as for specific classes of programs. Challenges regarding efficient evaluation of HEX-programs comprise the lack of a tight integration of the solving process with the evaluation of external sources and with the grounding procedure.
Accordingly, the main focus of this thesis is the design of advanced reasoning techniques that improve the evaluation of HEX-programs by tightly integrating processes which have so far been treated as mostly independent sub-problems. Moreover, all newly developed HEX-algorithms have been implemented in the state-of-the-art HEX-solver, and their performance has been empirically evaluated using a rich benchmark suite. Another focus of this thesis is on new applications, which leverage the expressiveness of the HEX-formalism and capabilities of its solvers, and in turn, push the advancement of the formalism. In this context, two innovative applications of HEX-programs that utilize external atoms for integrating as well as realizing methods from the area of machine learning are developed.