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.
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
|
Standard Resources by
Stuart F. Allen
Subject: Nuprl
Description: Standard library of Nuprl objects.
2003
|
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
|
Lists by
Stuart F. Allen
Subject:
Description: We emphasize here several sections of the library about the List data type.
2001
|
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
|
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
|
Fundamental Theorem of Arithmetic by
Stuart F. Allen
Subject: Arithmetic
Description: The Fundamental Theorem of Arithmetic - unique prime factorizability
2004
|
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
|
Russel's Paradox by
Stuart F. Allen
Subject: Logic
Description:
2004
|
How to browse the library by
Stuart F. Allen
Subject:
Description:
2004
|
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
|
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
|
Nuprl Editor and Interface by
Stuart F. Allen
Subject: Nuprl
Description: Editor Documentation from the nuprl_sfa interface to Nuprl4.
2003
|
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
|
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
|
Graph Theory by
Mark Bickford
Subject:
Description: This is Mark Bickford's formal library about the Graph Theory.
2003
|
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
|
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
|
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
|
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
|
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
|
An Intuitionistic Formalization of The Elements of Euclid Book I by
Ariel Kellison, Mark Bickford
Subject: Geometry
Description: A Nuprl formalization of Book I of the Elements of Euclid using intuitionistic primitives and axioms.
2019
|
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
|
Finite Automata by
Robert L. Constable
Subject: Logic
Description:
2001
|
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
|
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
|
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
|
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
|
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
|
Bar-Type Rules by
Karl Crary
Subject:
Description:
2002
|
Automatic FDL Projections by
Richard Eaton
Subject: Nuprl
Description: Collection of projections from the Formal Digital Library in 2006
2006
|
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
|
Work in Progress by
Richard Eaton
Subject: Nuprl
Description: a snapshot of Nuprl library objects
2012
|
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
|
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
|
Constructive General Algebra by
Paul B. Jackson
Subject: Arithmetic
Description:
1999
|
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
|
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
|
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
|
An Intuitionistic Formalization of The Elements of Euclid Book I by
Ariel Kellison, Mark Bickford
Subject: Geometry
Description: A Nuprl formalization of Book I of the Elements of Euclid using intuitionistic primitives and axioms.
2019
|
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
|
Intuitionistic Mathematics and Logic by
Joan Rand Moschovakis, Garyfallia Vafeiadou
Subject: Intuitionistic Mathematics
Description:
The first seeds of mathematical intuitionism germinated in Europe over a century ago in the constructive tendencies of Borel, Baire, Lebesque, Poincaré, Kronecker and others. The flowering was the work of one man, Luitzen Egbertus Jan Brouwer, who taught mathematics at the University of Amsterdam from 1909 until 1951. By proving powerful theorems on topological invariants and fixed points of continuous mappings, Brouwer quickly build a mathematical reputation strong enough to support his revolutionary ideas about the nature of mathematical activity. These ideas influenced Hilbert and Gödel and established intuitionistic logic and mathematics as subjects worthy of independent study
Our aim is to describe the development of Brouwer's intuitionism, from his rejection of the classical law of excluded middle to his controversial theory of the continuum, with fundamental consequences for logic and mathematics. We borrow Kleene's formal axiomatic systems (incorporating earlier attempts by Kolmogorov, Glivenko, Heyting and Peano) for intuitionistic logic and arithmetic as subtheories of the corresponding classical theories, and sketch his use of gödel numbers of recursive functions to realize sentences of intuitionistic arithmetic including a form of Church's Thesis. Finally, we present Kleene and Vesley's axiomatic treatment of Brouwer's continuum, with the function-realizability interpretation which establishes its consistency.
2020
|
Zeno by
Pavel Naumov
Subject:
Description:
2002
|
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
|
Turing Machine Basics by
Pavel Naumov
Subject: Logic
Description:
1996
|
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
|
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
|
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
|
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
|
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
|
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
|
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
|
Intuitionistic Mathematics and Logic by
Joan Rand Moschovakis, Garyfallia Vafeiadou
Subject: Intuitionistic Mathematics
Description:
The first seeds of mathematical intuitionism germinated in Europe over a century ago in the constructive tendencies of Borel, Baire, Lebesque, Poincaré, Kronecker and others. The flowering was the work of one man, Luitzen Egbertus Jan Brouwer, who taught mathematics at the University of Amsterdam from 1909 until 1951. By proving powerful theorems on topological invariants and fixed points of continuous mappings, Brouwer quickly build a mathematical reputation strong enough to support his revolutionary ideas about the nature of mathematical activity. These ideas influenced Hilbert and Gödel and established intuitionistic logic and mathematics as subjects worthy of independent study
Our aim is to describe the development of Brouwer's intuitionism, from his rejection of the classical law of excluded middle to his controversial theory of the continuum, with fundamental consequences for logic and mathematics. We borrow Kleene's formal axiomatic systems (incorporating earlier attempts by Kolmogorov, Glivenko, Heyting and Peano) for intuitionistic logic and arithmetic as subtheories of the corresponding classical theories, and sketch his use of gödel numbers of recursive functions to realize sentences of intuitionistic arithmetic including a form of Church's Thesis. Finally, we present Kleene and Vesley's axiomatic treatment of Brouwer's continuum, with the function-realizability interpretation which establishes its consistency.
2020
|
