An Infrastructure for Intertheory Reasoning

William M. Farmer

2000

Abstract

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.