A Set-theoretic Setting for Structuring Theories in Proof Development
Zhaohui Luo and Rod BurstallAbstract: We present a meta-setting for structured theory development in proof development systems, based on which a theory-structuring language S-CLEAR is defined. A frame is a logic endowed with a lattice structure and a renaming mechanism which capture the basic notions for structured theory development. Besides providing basic theory operations, S-CLEAR supports generic theories. An important feature is that type-checking for the application of a generic theory is decidable. Parameterization also supports structure sharing between theories. Theory bases may be built up using these mechanisms and used for structured development of large proofs. The semantics of S-CLEAR is very simple and logic-independent.
Previous | Index | Next