http:^^www.cs.cornell.edu^info^people^jackson^thesis^abstract.html

This data set contains WWW-pages collected from computer science departments of various universities

MIME-Version: 1.0
Server: CERN/3.0
Date: Sunday, 24-Nov-96 19:07:35 GMT
Content-Type: text/html
Content-Length: 2752
Last-Modified: Monday, 10-Apr-95 18:02:29 GMT

<title> Abstract for Paul Jackson's PhD Thesis </title>

<h1>Thesis Abstract</h1>
<p>
ENHANCING THE NUPRL PROOF DEVELOPMENT SYSTEM AND
APPLYING IT TO COMPUTATIONAL ABSTRACT ALGEBRA
<p>
Paul Bernard Jackson, Ph.D.
<p>
Cornell University 1995

<hr>

This thesis describes substantial enhancements that were made to the
software tools in the Nuprl system that are used to interactively
guide the production of formal proofs. Over 20,000 lines of code were
written for these tools.  Also, a corpus of formal mathematics was
created that consists of roughly 500 definitions and 1300 theorems.
Much of this material is of a foundational nature and supports all
current work in Nuprl.  This thesis concentrates on describing the
half of this corpus that is concerned with abstract algebra and that
covers topics central to the mathematics of the computations carried
out by computer algebra systems.
<p>
The new proof tools include those that solve linear arithmetic
problems, those that apply the properties of order relations, those
that carry out inductive proof to support recursive definitions, and
those that do sophisticated rewriting.  The rewrite tools allow
rewriting with relations of differing strengths and take care of
selecting and applying appropriate congruence lemmas automatically.
The rewrite relations can be order relations as well as equivalence
relations. If they are order relations, appropriate monotonicity
lemmas are selected.
<p>
These proof tools were heavily used throughout the work on
computational algebra. Many examples are given that illustrate their
operation and demonstrate their effectiveness.
<p>
The foundation for algebra introduced classes of monoids, groups,
rings and modules, and included theories of order relations and
permutations.  Work on finite sets and multisets illustrates how a
quotienting operation hides details of datatypes when reasoning about
functional programs.  Theories of summation operators were developed
that drew indices from integer ranges, lists and multisets, and that
summed over all the classes mentioned above.  Elementary factorization
theory was developed that characterized when cancellation monoids are
factorial.  An abstract data type for the operations of multivariate
polynomial arithmetic was defined, and the correctness of an
implementation of these operations was verified. The implementation is
similar to those found in current computer algebra systems.
<p>
This work was all done in Nuprl's constructive type theory. 
The thesis discusses the appropriateness of this foundation, and
the extent to which the work relied on it.
<hr>
Last Modified Jan 20th, 1995<p>

<address> Paul Jackson / <a href="mailto:[e-mail]">[e-mail]</a> </address>