http:^^www.cs.cornell.edu^info^people^jackson^nuprl^index.html

来自「This data set contains WWW-pages collect」· HTML 代码 · 共 115 行

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

<title>Summary of Nuprl Theories</title>
<hr>
<h1> Summary of Theories</h1>
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
<a href="format.html"> here.</a>
<hr>
<dl>
<dt>
<a href="theories/core_1.html"> <b>core_1</b></a> (18, 0, 0)
<dd>
Display forms for primitive terms of type-theory. Abstractions for  
propositions-as-types correspondence. Parenthesization control. 
<dt>
<a href="theories/core_2.html"> <b>core_2</b></a> (40, 102, 347)
<dd>
General-purpose definitions and 
theorems.
<dt>
<a href="theories/well_fnd.html"> <b>well_fnd</b></a> (1, 6, 129)
<dd>
Well-founded predicate. Rank induction lemmas and 
tactics. 
<dt>
<a href="theories/int_1.html"> <b>int_1</b></a> (9, 33, 169)
<dd>
Integer inequalities, subtypes, and  
induction lemmas for subtypes.
<dt>
<a href="theories/bool_1.html"> <b>bool_1</b></a> (17, 67, 239)
<dd>
Definitions, theorems and tactics for the boolean  
type and boolean-related expressions. 
<dt>
<a href="theories/fun_1.html"> <b>fun_1</b></a> (9, 21, 106)
<dd>
Polymorphic identity and composition functions.  
Lemmas covering properties suchas injectivity and  
surjectivity.
<dt>
<a href="theories/int_2.html"> <b>int_2</b></a> (9, 143, 937)
<dd>
Defines mod, floor, max and min functions over the  
integers. 
Lemmas concern basic properties of arithmetic functions over integers, and induction principles. 
<dt>
<a href="theories/list_1.html"> <b>list_1</b></a> (16, 54, 315)
<dd>
<dt>
<a href="theories/gen_algebra_1.html"> <b>gen_algebra_1</b></a> (51, 144, 464)
<dd>
Properties of order and equivalence relations, 
and of algebraic functions (e.g. commutativity 
associativity).   
 
<dt>
<a href="theories/sets_1.html"> <b>sets_1</b></a> (18, 52, 133)
<dd>
Family of classes for types with computable equality and 
inequality relations. 
<dt>
<a href="theories/groups_1.html"> <b>groups_1</b></a> (50, 199, 752)
<dd>
Family of classes for monoids and groups. 
Summations with indices from integer subranges. Exponential functions.
<dt>
<a href="theories/perms_1.html"> <b>perms_1</b></a> (21, 80, 623)
<dd>
<dt>
<a href="theories/perms_2.html"> <b>perms_2</b></a> (5, 34, 422)
<dd>
Introduces the binary relations on lists `is a permutation of', 
`is a permutation of up to', and `is equivalent up to'.
<dt>
<a href="theories/list_2.html"> <b>list_2</b></a> (21, 94, 638)
<dd>
Introduces a variety of standard list-related functions, 
that assume that list elements come from a type 
or monoid with decidable equality.
<dt>
<a href="theories/rings_1.html"> <b>rings_1</b></a> (44, 126, 376)
<dd>
Family of classes for rings, integral domains  
and fields. Ideals and quotient rings. Sums and products.
<dt>
<a href="theories/mset.html"> <b>mset</b></a> (25, 112, 592)
<dd>
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.  
<dt>
<a href="theories/factor_1.html"> <b>factor_1</b></a> (16, 61, 386)
<dd>
Divisibility theory for monoids with cancellation.  
Develops theorems characterizing when factorizations are 
unique and derives from these the fundamental theorem of 
arithmetic.
</dl>
<hr>
Last modified February 24th, 1995
<p>
<address>
Paul Jackson /
<a href="mailto:[e-mail]"> [e-mail]</a>
</address>