MIME-Version: 1.0 Server: CERN/3.0 Date: Sunday, 24-Nov-96 19:07:05 GMT Content-Type: text/html Content-Length: 3468 Last-Modified: Monday, 27-Feb-95 02:06:56 GMT Summary of Nuprl Theories

Summary of Theories

Each link below leads to a formatted presentation of a Nuprl theory. A description of the organization of these presentations and of the meaning of the triples after each link name can be found here.
core_1 (18, 0, 0)
Display forms for primitive terms of type-theory. Abstractions for propositions-as-types correspondence. Parenthesization control.
core_2 (40, 102, 347)
General-purpose definitions and theorems.
well_fnd (1, 6, 129)
Well-founded predicate. Rank induction lemmas and tactics.
int_1 (9, 33, 169)
Integer inequalities, subtypes, and induction lemmas for subtypes.
bool_1 (17, 67, 239)
Definitions, theorems and tactics for the boolean type and boolean-related expressions.
fun_1 (9, 21, 106)
Polymorphic identity and composition functions. Lemmas covering properties suchas injectivity and surjectivity.
int_2 (9, 143, 937)
Defines mod, floor, max and min functions over the integers. Lemmas concern basic properties of arithmetic functions over integers, and induction principles.
list_1 (16, 54, 315)
gen_algebra_1 (51, 144, 464)
Properties of order and equivalence relations, and of algebraic functions (e.g. commutativity associativity).
sets_1 (18, 52, 133)
Family of classes for types with computable equality and inequality relations.
groups_1 (50, 199, 752)
Family of classes for monoids and groups. Summations with indices from integer subranges. Exponential functions.
perms_1 (21, 80, 623)
perms_2 (5, 34, 422)
Introduces the binary relations on lists `is a permutation of', `is a permutation of up to', and `is equivalent up to'.
list_2 (21, 94, 638)
Introduces a variety of standard list-related functions, that assume that list elements come from a type or monoid with decidable equality.
rings_1 (44, 126, 376)
Family of classes for rings, integral domains and fields. Ideals and quotient rings. Sums and products.
mset (25, 112, 592)
Finite multisets and finite sets. Summation with indices drawn from multisets. Defines ADT for free abelian monoids, and demonstrates an instance of this ADT using multisets.
factor_1 (16, 61, 386)
Divisibility theory for monoids with cancellation. Develops theorems characterizing when factorizations are unique and derives from these the fundamental theorem of arithmetic.

Last modified February 24th, 1995

Paul Jackson / jackson@cs.cornell.edu