非表示:
キーワード:
-
要旨:
Decision procedures are key components of theorem provers and
constraint satisfaction systems. Their modular combination is of
prime interest for building efficient systems, but their effective
use is often limited by poor interface capabilities, when such
procedures only provide a simple ``sat/unsat'' answer. In this
paper, we develop a framework to design cooperation schemas between
such procedures while maintaining modularity of their
interfaces. First, we use the framework to specify and prove the
correctness of classic combination schemas by Nelson-Oppen and
Shostak. Second, we introduce the concept of deduction complete
satisfiability procedures, we show how to build them for large
classes of theories, then we provide a schema to modularly
combine them. Third, we consider the problem of modularly
constructing explanations for combinations by re-using available
proof-producing procedures for the component theories.
