An Infrastructure for Intertheory Reasoning

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.

• Type: Conference
• Year: 2000
• Where: CADE
• Authors: William M. Farmer
• Keywords: CADE 2000, Infrastructure Includes Machinery, Intertheory Reasoning, Little Theories Method, Logical Reasoning