Subject: System

Keywords: ::overview

Title: System Overview

--------------------------------------------------
Proofs as a Service

Nuprl has three main components: 
library, refiners, and editors.

The library can be further divided into database,
transaction manager, and orchestration. There is a 
single library, but it can be replicated.
There can be many individual refiners and editors. 
Each replicated library instance can support more than
one hundred refiners.

All content is stored as objects. The library
maintains an association of object ids to their content.
Formal content includes definitions, lemmas, proofs, and rules.
Informal content includes tactics, procedures, display rules, and
content organization.

A proof is a top down refinement tree. A node of the tree consists
of a goal, a tactical expression, and the subgoals produced by 
refining the goal using the tactic expression. A tactical expression
is a tree of tactic expressions. A tactic expression is a tactic
function along with argument instances. A tactic function is a function
which applies rules to goals.  
 
Formal content is organized in theories. A theory is an ordered list
of definitions, lemmas, and tactic code. Each theory specifies
prerequisite theories. Thus the context needed to perform a refinement
is determinable by specifying an object in a theory. Then any
preceding object is available to be used during the refinement. 
In this way, each proof node is separately evaluable from the rest.
Thus multiple refiners may be used simultaneously to work on separate
subtrees of a proof.

Nuprl is a dynamic system. Tactic code is frequently modified. 
Theories are frequently extended. Lemmas can be modified. Theories
are allowed to become inconsistent. A process of Replay, Rebuild, 
and Repair is used to re-establish the consistency of the formal
content. Replay is used to identify proof nodes which no longer
produce the same subgoals. Rebuild attempts to make new proof trees
by re-using the original proof's tactic expressions. Repair does further
searching to attempt automatically repair incomplete proofs. 

Nuprl leverages its separate refinement ability and many refiners
to perform most of these operations concurrently. Current work on
the system is focused on improving the effectiveness of the 
repair facility. This is being done by breaking up the tactic 
expression in a proof node to make more but simpler nodes. 
These simpler nodes are then instrumented and generalized to make
them more reusable. These features free proof authors to modify
theories with confidence that they can easily repair content
broken by modifications.  
⋅
--------------------------------------------------

Authors: NUPRL:t

⋅

Home