An Infrastructure for Intertheory Reasoning

The little theories method, in which mathematical reasoning is distributed across a network of theories, is a powerful technique for describing and analyzing complex systems. This paper presents an infrastructure for intertheory reasoning that can support applications of the little theories method. The infrastructure includes machinery to store theories and theory interpretations, to store known theorems of a theory with the theory, and to make definitions in a theory by extending the theory “in place”. The infrastructure is an extension of the intertheory infrastructure employed in the IMPS Interactive Mathematical Proof System.