Next:
7. Logic Overview
Up:
The IMPS User's Manual
Previous:
6. Little Theories
2. User's Guide
7. Logic Overview
7.1 Introduction
7.2 Languages
7.3 Semantics
7.4 Extensions of the Logic
7.5 Hints and Cautions
8. Theories
8.1 Introduction
8.2 How to Develop a Theory
8.3 Languages
8.4 Theorems
8.5 Definitions
8.6 Theory Libraries
8.7 Hints and Cautions
9. Theory Interpretations
9.1 Introduction
9.2 Translations
9.3 Building Theory Interpretations
9.4 Translation of Defined Sorts and Constants
9.5 Reasoning and Formalization Techniques
9.6 Hints and Cautions
10. Quasi-Constructors
10.1 Motivation
10.2 Implementation
10.3 Reasoning with Quasi-Constructors
10.4 Hints and Cautions
11. Theory Ensembles
11.1 Motivation
11.2 Basic Concepts
11.3 Usage
11.4 Def-theory-ensemble
11.5 Def-theory-multiple
11.6 Def-theory-ensemble-instances
11.7 Def-theory-ensemble-overloadings
11.8 Hints and Cautions
12. The Proof System
12.1 Proofs
12.2 The IMPS Proof System
12.3 Theorem Proving
12.4 The Script Language
12.5 The Script Interpreter
12.6 Hints and Cautions
13. Simplification
13.1 Motivation
13.2 Implementation
13.3 Transforms
13.4 Algebraic Processors
13.5 Hints and Cautions
14. Macetes
14.1 Classification
14.2 Atomic Macetes
14.3 Compound Macetes
14.4 Building Macetes
14.5 Applicable Macetes
14.6 Hints and Cautions
15. The Iota Constructor
15.1 Motivation
15.2 Reasoning with Iota
15.3 Hints and Cautions
16. Syntax: Parsing and Printing
16.1 Expressions
16.2 Controlling Syntax
16.3 String Syntax
16.4 Parsing
16.5 Modifying the String Syntax
16.6 Hints and Cautions
Next:
7. Logic Overview
Up:
The IMPS User's Manual
Previous:
6. Little Theories
System Administrator
2000-07-23
