Skip to main content
PRL Project

PRL Math Library

Recent Library Updates

This is a library of fully formalized definitions and proofs. Some of the material has been enhanced by the addition of informal explanations referring to it.

Tips for browsing the library

Browse by shelf view | orig sort | title | date | author | subject

42 results

        Full Nuprl Library

A Fast Algorithm for the Integer Square Root
by
Anne Trostle, Mark Bickford

Subject: Arithmetic
Description:

The integer square root of a natural number can be solved using many different algorithms which differ in level of efficiency. We discuss several of these algorithms and include a detailed account of a constructive proof using fast induction. We also introduce the concept of constructive real numbers and relate the integer square root to the real square root.

2014


A Formal Exploration of Constructive Geometry
by
Sarah Sernaker, Robert L. Constable

Subject:
Description:

We investigated synthetic geometry and propositions from Euclid's Elements using constructive mathematics and utilizing results from Beeson, Tarski, Hilbert, and Euclid.



2016


An Algorithm for the Greatest Common Divisor
by
Anne Trostle

Subject: Arithmetic
Description:

This page shows existence proofs and recursive algorithms in Nuprl for the greatest common divisor of two natural numbers.

2013


Automatic FDL Projections
by
Richard Eaton

Subject: Nuprl
Description: Collection of projections from the Formal Digital Library in 2006

2006


Bar-Type Rules
by
Karl Crary

Subject:
Description:

2002


Chain Replication Protocol
by
Mark Bickford

Subject: Systems
Description: This book collects materials used in the formalization of an important distributed algorithm, by Schneider and van Renesse, called Chain Replication. The chain replication algorithm provides a fault-tolerant distributed storage system and guarantees a strong consistency property.

2006


Classical Propositional Logic
by
James L. Caldwell

Subject: Logic
Description: We describe a formal constructive proof of the decidability of a sequent calculus for classical propositional logic. The proof is implemented in the Nuprl system and the resulting proof object yields a correct-by-construction program for deciding propositional sequents.

2004


Collaborative Mathematics Environments
by
Robert L. Constable

Subject: Systems
Description: Written with Paul Chew, Keshav Pingali, Steve Vavasis, Richard Zippel

Computational science will be the dominant paradigm for science in the next century. This proposal addresses one of the major challenges facing this new kind of science---the demand for better software support for computational mathematics. The task of providing this support is sufficiently central to the national interest and sufficiently comprehensive that it could serve as a Grand Challenge problem for computer science.

1996


Constructive Factorization Theory
by
Paul B. Jackson

Subject: Arithmetic
Description: Introduces the theory of divisibility in cancellation monoids, and builds up to theorem characterizing when unique factorizations exist and are unique.

The theory here is developed constructively. Some theorems computable content is 'useful': e.g. mfact_exists. An instantiation of this theorem is posint_is_ufm, which has as extract, a theorem to compute prime factorisations. Other theorems have computational content which is for most purposes uninteresting. e.g. look at theorem unique_mfact.

The theorem unique_mfact nicely demonstrates rewriting with equivalence relations of differing strengths: e.g. permr and permr_upto.

1999


Constructive General Algebra
by
Paul B. Jackson

Subject: Arithmetic
Description:

1999


Constructive Reading of Classical Logic
by
Robert L. Constable, Sarah Sernaker

Subject:
Description:

Using the implementation of virtual evidence, Nuprl can constructively prove classical theorems.

2015


Discrete Math Materials
by
Stuart F. Allen

Subject: Arithmetic
Description: Counting is finding a function of a certain kind.



When we count a class of objects, we generate an enumeration of them, which we may represent by a One-to-One Correspondence from a standard class having that many objects to the class being counted. Our standard class of n objects, for n  , will be n, which is the class {k:| 0  k < n } of natural numbers less than n. A more familiar choice of standard finite classes might have been {k:| 1  k  n }, but there is also another tradition in math for using {k:| 0  k < n }.




2004


Elementary Number Theory
by
Stuart F. Allen

Subject: Arithmetic
Description: Elementary divisibility theory over the integers. Gcd function and relation introduced. Chinese remainder theorem proven.

2003


Event Systems
by
Mark Bickford

Subject: Systems
Description: This is Mark Bickford's formal library about the Event Systems developed by him and Robert Constable.

2003


Finding the Maximum Segment Sum
by
Anne Trostle

Subject: Arithmetic
Description:

The problem of finding the maximum segment sum for a given sequence of numbers is useful for illustrating several key concepts in programming, such as writing specifications, utilizing dependent types, and showing how proofs reveal programs and programs reveal proofs. In this account of the problem, we describe an algorithm for finding the solution and then show its proof in Nuprl.


2014


Finite Automata
by
Robert L. Constable

Subject: Logic
Description:

2001


Finite Multi-Sets
by
Paul B. Jackson

Subject:
Description: Nuprl's quotient type is used to construct a type of finite multisets from the type of lists. Standard functions over multisets are introduced, including a summation function that draws indices from finite multisets.

A definition is given of a free abelian monoid ADT, and an instance of this ADT is constructed using the multiset functions.

Finite sets are defined as a subtype of finite multisets, and the usual set operations are introduced.

1999


Formalizing Constructive Analysis in Nuprl
by
Mark Bickford

Subject: Arithmetic
Description: Mark Bickford has been formalizing Chapter Two of Constructive Analysis in Nuprl, creating detailed definitions and proofs.

2012


Formalizing Moessner's Theorem in Nuprl
by
Mark Bickford, Dexter Kozen, Alexandra Silva

Subject: Logic
Description: Moessner's theorem describes a procedure for generating a sequence of n integer sequences that lead unexpectedly to the sequence of nth powers 1n, 2n, 3n, ... . Several generalizations of Moessner's theorem exist. Recently, Kozen and Silva gave an algebraic proof of a general theorem that subsumes Moessner's original theorem and its know generalizations. In this note, we describe the formalization of this theorem that the first author did in Nuprl.

2012


Fundamental Theorem of Arithmetic
by
Stuart F. Allen

Subject: Arithmetic
Description: The Fundamental Theorem of Arithmetic - unique prime factorizability

2004


General Automata Theory
by
Mark Bickford

Subject: Systems
Description: General (infinite-state) transition systems are defined using records. This makes it possible to define intersection and renaming operations on the transition systems, which we call state-machines, and these operations have nice properties. We define notions such as reachable states, invariants, stable properties, etc. and prove theorems about their preservation under intersection and renaming.

2003


Graph Theory
by
Mark Bickford

Subject:
Description: This is Mark Bickford's formal library about the Graph Theory.

2003


HOL Translation (partial)
by
Douglas J. Howe

Subject: Nuprl
Description: This is part of Doug Howe's HOL library.

It modifies the Nuprl logic to make HOL interpretable.

This translation is based upon Howe's Importing Mathematics from HOL into Nuprl.

2004


How to browse the library
by
Stuart F. Allen

Subject:
Description:

2004


Hybrid Protocols
by
Mark Bickford

Subject: Systems
Description: We describe a generic switching protocol for the construction of hybrid protocols and prove it correct with the proof development system. We introduce the concept of meta-properties to characterize communication properties that can be preserved by switching and identify switching invariants that an implementation of the switching protocol must satisfy in order to work correctly.

2002


Introduction to EventML
by
Mark Bickford, Robert L. Constable, Richard Eaton, David Guaspari

Subject: Nuprl
Description: EventML is a functional programming language in the ML family, closely related to Classic ML. It is also a language for coding distributed protocols (such as Paxos [Ren11]) using high level combinators from the Logic of Events (or Event Logic), hence the name EventML.

EventML was also created to work in cooperation with an interactive theorem prover and to be a key component of a Logical Programming Environment (LPE).

This tutorial also includes multiple example protocols, including ping pong, 2/3 consensus, and Paxos (coming soon).

2012


Iterated Binary Operations
by
Stuart F. Allen

Subject: Systems
Description: This section treats the iteration of binary operations over values indexed indexed by finite integer subranges. We parameterize iteration by the binary operation and a value, typically its identity element, for the empty range. Here are some familiar special cases.

2004


Lists
by
Stuart F. Allen

Subject:
Description: We emphasize here several sections of the library about the List data type.

2001


Logical Investigations, with the Nuprl Proof Assistant
by
Robert L. Constable, Anne Trostle

Subject: Logic
Description: An introduction to concepts in First-Order Logic, illustrated using proofs from Nuprl

2014


Nuprl Basics
by
Stuart F. Allen

Subject: Nuprl
Description: Basic concepts and methods used for mathematical expressions in Nuprl. The primitive operators as well as basic nonprimitives are discussed.

2003


Nuprl Editor and Interface
by
Stuart F. Allen

Subject: Nuprl
Description: Editor Documentation from the nuprl_sfa interface to Nuprl4.

2003


Permutations vol. 1
by
Paul B. Jackson

Subject:
Description:

1999


Permutations vol. 2
by
Paul B. Jackson

Subject:
Description: Defines several equivalence relations on lists, including 'is a permutation of', 'is a permutation of up to', and 'is equivalent to, up to'.

The permutation relations were defined in terms of permutation functions. This turned out to be rather awkward. Would have been much easier to start with computable notions of when one list is a permutation of another (see list_2 for details).

Various properties of these relations were proven.

1999


Readability Exercise (num theory)
by
Stuart F. Allen

Subject: Arithmetic
Description: Number Theory Examples

Here are several examples of proofs about numbers. Each consists of a formal proof and an informal gloss of it.

2004


Russel's Paradox
by
Stuart F. Allen

Subject: Logic
Description:

2004


Simple Imperative Programming
by
Pavel Naumov

Subject: Systems
Description: Simple Imperative Programming Language library is a collection of Nuprl theories that formalize syntax and semantics of a simple imperative programming language.

2002


Square Root of 2 is Irrational
by
Stuart F. Allen

Subject: Arithmetic
Description: Here we give formal proofs along with informal glosses of proofs to the effect that 2 has no rational square root, and more generally, that no prime number has a rational square root.
The proof about 2 is simpler, of course, and so is a better approach to the one about primes.

2004


Standard Resources
by
Stuart F. Allen

Subject: Nuprl
Description: Standard library of Nuprl objects.

2003


Towers of Hanoi
by
Stuart F. Allen

Subject: Puzzels
Description: Towers of Hanoi: a thorough treatment.
The purpose of these notes is to exhibit the application of formal proof-oriented methods to a familiar non-trivial problem.

2004


Turing Machine Basics
by
Pavel Naumov

Subject: Logic
Description:

1996


Work in Progress
by
Richard Eaton

Subject: Nuprl
Description: a snapshot of Nuprl library objects

2012


Zeno
by
Pavel Naumov

Subject:
Description:

2002


Website feedback
PRL Project   |   Computer Science Department   |   Cornell University
nuprl@cs.cornell.edu   |   320 Gates Hall, Ithaca, NY 14853   |   © 2014 Cornell University
site admin | Prof Constable's Library | PRL SourceForge Project Page