Propagators and Solvers for the Algebra of Modular Systems

Complex artifacts are, of necessity, constructed by assembling simpler components. Software systems use libraries of reusable components, and often access multiple remote services. In this paper, we consider systems that can be formalized as solving the model expansion task for some class of finite structures. A wide range of problem solving and query answering systems are so accounted for. We present a method for automatically generating a solver for a complex system from a declarative definition of that system in terms of simpler modules, together with solvers for those modules. The work is motivated primarily by "knowledge-intensive" computing contexts, where the individual modules are defined in (possibly different) declarative languages, such as logical theories or logic programs, but can be applied anywhere the model expansion formalization can. The Algebra of Modular Systems (AMS) [48, 49], provides a way to define a complex module in terms of a collection of other modules, in purely semantic terms. Formally, each module in this algebra represents a class of structures, and a "solver" for the module solves the model expansion task for that class. That is, a solver for module M takes as input a structure A for a part of the vocabulary of M, and returns either a set of expansions of A that are in M, or the empty set.