Modular Equivalence in General
Tomi Janhunen · Frontiers in artificial intelligence and applications · 2008
The notion of modular equivalence was recently introduced in the context of a module architecture proposed for logic programs under answer set semantics [12, 6, 13]. In this paper, the module architecture is abstracted for arbitrary knowledge bases, KB-functions for short, giving rise to a universal notion of modular equivalence. A further objective of this paper is to study modular equivalence in the contexts of SAT-functions, i.e., propositional theories with a module interface, and their logic programming counterpart, known as LP-functions [6]. As regards SAT-functions, we establish the full compositionality of classical semantics. This proves modular equivalence a proper congruence relation for SAT-functions. Moreover, we address the interoperability of SAT-functions and LP-functions in terms of strongly faithful transformations in both directions. These considerations justify the proposed design of KB-functions in general and pave the way for hybrid KB-functions.