Modular nonmonotonic logic programs

Abstract

Modular programming is common practice in software development, and the vast majority of general-purpose programming languages use modularity concepts to aid software engineers in designing and building complex systems based on reusable software components. Answer Set Programming (ASP), in comparison, is a popular paradigm for declarative programming and knowledge representation, but methods for reusing subprograms and program elements in ASP have not arrived for common use yet. This thesis proposes Modular Nonmonotonic Logic Programs (MLPs), which are disjunctive logic programs under answer set semantics with modules that have contextualized input. Such programs incorporate a call by value mechanism and allow for unrestricted calls between modulesincluding mutual and self recursionas a new approach to extend ASP with module constructs akin to those found in conventional programming. We define a model-theoretic semantics for this extended setting, show that many desired properties of ordinary logic programming generalize to modular ASP, and determine the computational complexity of the new formalism. For the purpose of implementation, we consider rewriting techniques that make MLP semantics amenable to off-the-shelf ASP solvers. We present translations that take an MLP with module input and rewrite them in stages to a combined logic program without input that is evaluable with ASP reasoners. This operation comes at the price of inflating the program exponentially, but complexity-theoretic assumptions suggest that this is unavoidable. The alternative macro expansion technique applicable to syntactically restricted MLPs does not incur the blowup observable in the general setting, and we make use of it to develop an application by embedding hybrid Description Logic Programs into MLPs. This effectively unites MLP with established Datalog engines as backbone for the computation, which we experimentally evaluate. We characterize answers sets in terms of classical (Herbrand) models of propositional, first-, and second-order sentences, extending a line of research for conventional logic programs. To this end, we lift on one side well-known loop formulas to MLPs, and otherwise augment ordered program completion for MLPs, which avoids explicit loop formula construction by auxiliary predicates. A further result is a study on the relationship of MLPs and DLP-functions, which is a notable formalism for compositional modular ASP with well-defined input/output interface. These investigations widen our understanding of MLPs and may prove beneficial for further semantic analysis and implementation perspectives.