The Architecture of Inference from SMT to ETB
Modularity plays a central role in logical reasoning. We want to beable to reuse proofs, proof patterns, theories, and specializedreasoning procedures. Architectures that support modularity have beendeveloped at all levels of inference: SAT solvers, theory solvers,combination solvers and rewriters, SMT solvers, simplifiers, rewriters,and tactics-based interactive theorem provers. Prior work has mostlyfocused on fine-grained modular inference. However, with theavailability of a diverse range of high-quality inference tools, it hasbecome important to systematically integrate these big components intorobust toolchains. At SRI, we have been developing a framework calledthe Evidential Tool Bus (ETB) as a distributed platform for thecoarse-grained integration of inference components into flexible,scriptable workflows. The talk describes the architecture of ETB alongwith some motivating applications.