Introduction -- Nature of the PRL Project

New to PRL? Start with the Introduction and the first chapters of the Nuprl book. These introductions include many links to other material located at the web site.

• The Nuprl book
• Origins of the PRL Project
• Goals
• Dynamics of the Project
• Mathematical Expression in Nuprl

Project Focus

The project remains focused on logic-based tools to support programming and on implementing formal computational mathematics; we see these as inextricably linked activities. Over the years the scope of the project has expanded - from developing individual programs and theorems to constructing systems and theories. Starting with the slogan "proofs-as-programs," we now talk about "theories-as-systems." This change of scale has led to a new class of problems and challenges discussed throughout this project summary.

Goals

We are currently focused on these goals:

• Build proof assistants that are as indispensable to programmers and mathematicians as word processors are now.
• Design and implement proof assistants that consistently exhibit problem solving behavior considered "intelligent" - in the sense that Deep Blue is an "intelligent" chess player.
• Create consistent standard formalizations of the core mathematics that are widely assumed as background in computing and mathematics education at the college level and that are frequently used in designing algorithms and systems.
• Provide convenient access to the digital libraries of formalized mathematics mentioned just above that is so useful that the formal material becomes a standard reference for mathematical knowledge and is widely cited in textbooks.

More details on project goals »

Technical Content and Cross Links

The project is multi-faceted. One way to understand it is to see its projections onto other areas of computer science and mathematics. The standard projections are onto these topics:

• Applications
• Artificial Intelligence (AI)
• Automated Deduction (AD)
• Constructive Mathematics
• Education
• Formal Methods
• Formalized Mathematics (AutoMath)
• Human Computer Interface
• Logic
• Philosophy of Mathematics
• Problem Solving Environments (PSE)
• Programming Languages
• Program Synthesis
• Proof Technology
• Logical Programming Environments
• Software Engineering
• Systems
• Theory
• Type Theory, Set Theory and Domain Theory