Next:
List of Tables
Up:
The IMPS User's Manual
Previous:
The IMPS User's Manual
Contents
Contents
List of Tables
List of Figures
1. Introductory Material
1. Introduction
1.1 Overview of the Manual
1.2 Goals
1.2.1 Support for the Axiomatic Method
1.2.2 Logic
1.2.3 Computation and Proof
1.3 Components of the System
1.3.1 Core
1.3.2 Supporting Machinery
1.3.3 User Interface
1.3.4 Theory Library
1.4 Acknowledgments
2. Distribution
2.1 How to Get and Install IMPS
2.1.1 How to Get IMPS
2.1.2 How to Install IMPS
2.1.3 Instructions for IMPS Users
2.1.4 How to Start IMPS
2.1.5 The IMPS User's Manual
2.1.6 IMPS Papers
2.1.7 Bug Reports and Questions
2.2 IMPS Copyright Notice
3. A Brief Tutorial
3.1 Interacting with IMPS
3.2 On-line Documentation
3.3 Languages and Theories
3.4 Syntax
3.5 Proofs
3.6 Extending IMPS
3.7 The Little Theories Style
4. On-Line Help
4.1 The Manual
4.2 Def-forms
4.3 Using Menus
5. Exercises
5.1 Introduction
5.1.1 How to Use an Exercise
5.1.2 Paths Through the Exercises
5.2 Mathematical Exercises
5.2.1 Primes
5.2.2 A Very Little Theory of Differentiation
5.2.3 Monoids
5.2.4 Some Theorems on Limits
5.2.5 Banach's Fixed Point Theorem
5.2.6 Basics of Group Theory
5.3 Logical Exercises
5.3.1 Indicators: A Representation of Sets
5.3.2 Temporal Logic
5.4 Exercises related to Computer Science
5.4.1 The World's Smallest Compiler
5.4.2 A Linearization Algorithm for a Compiler
5.4.3 The Bell-LaPadula Exercise
6. Little Theories
2. User's Guide
7. Logic Overview
7.1 Introduction
7.2 Languages
7.2.1 Sorts
7.2.2 Expressions
7.2.3 Alternate Notation
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.5.1 Transporting Theorems
9.5.2 Polymorphism
9.5.3 Symmetry and Duality
9.5.4 Problem Transformation
9.5.5 Definition Transportation
9.5.6 Theory Instantiation
9.5.7 Theory Extension
9.5.8 Model Conservative Theory Extension
9.5.9 Theory Ensembles
9.5.10 Relative Satisfiability
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.3.1 Checking Proofs in Batch
12.4 The Script Language
12.4.1 Evaluation of Script Expressions
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.2.1 Schematic Macetes
14.2.2 Nondirectional 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.2.1 eliminate-defined-iota-expression
15.2.2 eliminate-iota
15.2.3 eliminate-iota-macete
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
3. Reference Manual
17. The IMPS Special Forms
17.1 Creating Objects
17.2 Changing Syntax
17.3 Loading Sections and Files
17.4 Presenting Expressions
18. The Proof Commands
19. The Primitive Inference Procedures
20. The Initial Theory Library: An Overview
Bibliography
Next:
List of Tables
Up:
The IMPS User's Manual
Previous:
The IMPS User's Manual
System Administrator
2000-07-23
