IMPS Theory Library Summary
Copyright (c) 1990-1994 The MITRE Corporation
Authors: W. Farmer, J. Guttman, F. J. Thayer
The IMPS theory library is a collection of theories, theory
interpretations, and theory constituents (e.g., definitions and
theorems) which serves as a database of mathematics. It is intended
to provide you with a starting point for building your own theory
library. It also is a source of examples that illustrates some of the
diverse ways mathematics can be formulated in IMPS .
This page contains only a sampling of the sections that are
contained in the IMPS initial theory library with a partial
description of each section.
Abstract Calculus
The main theory of this section is normed-spaces . The
section develops the basic notions of calculus (e.g., the derivative
and the integral) in the context of normed spaces. For relevant files
see normed spaces and metric-spaces
The Banach Contractive Fixed Point Theorem
This section has a proof of the Banach contractive mapping fixed point
theorem, which states that any contractive mapping on a complete
metric space has a unique fixed point. See fixed-point-theorem .
Basic Cardinality
This section introduces the basic notions of cardinality. It also
proves some basic theorems about finite cardinality such as the fact
that every subset of a finite set is itself finite. See various files defining this theory.
Basic Monoids
This section contains the theories monoid-theory and
commutative-monoid-theory . In monoid-theory a
constant monoid%prod is defined recursively as the iterated
product of the primitive monoid operation. Basic properties of this
constant are proved in monoid-theory and then are
transported to theories with their own iterated product operators,
such as h-o-real-arithmetic with the operators of sequence summation and product.
Binary Relations
Binary relations are represented in this section as certain partial
functions in the same way that sets are represented as indicators.
Several basic operations on binary relations are formalized as
quasi-constructors. As an exercise, the transitive closure of the
union of two equivalence relations is shown to be an equivalence
relation.
Counting Theorems for Groups
This section contains a proof of the fundamental counting theorem for
group theory. Several consequences of this theorem are proved
including Lagrange's theorem.
CSP
This section develops a new approach to process algebra and CSP which
departs from the usual formulations in which external behaviors are
modeled as sequences of events called traces.
Foundation
This section is always loaded with IMPS . It contains the
theory h-o-real-arithmetic and a number of definitions,
theorems, and macetes in this theory. It also adds a number of
definitions and theorems from a number of ``generic theories.''
h-o-real-arithmetic is an axiomatization of the real numbers
which we consider to be our working theory of the real numbers. The
theory h-o-real-arithmetic is equipped with routines for
simplifying arithmetic expressions and rational linear inequalities.
These routines allow the system to perform a great deal of low-level
reasoning without user intervention. See the various files defining the section.
Knaster Fixed Point Theorem
The main interest of this section is the statement and proof of the
Knaster fixed point theorem which states that on a complete partial
order with a least element and a greatest element, any monotone
mapping has a fixed point. One important application of this result
included in this section is a proof of the Schroeder-Bernstein
theorem.
Number Theory
This section develops the rudiments of number theory. The fundamental
theorem of arithmetic and the infinity of primes are proved.
_______________________________________________________
This page designed and maintained by F. Javier Thayer Fábrega
jt@mitre.org