TPHOLs 2003 Tutorial
Introduction to MetaPRL Theorem Prover
TPHOLs 2003 Tutorial
| |
MetaPRL is the latest system to come out of the Cornell PRL project. While written from scratch, it builds upon many ideas and techniques developed for its predecessor, the NuPRL system.
MetaPRL is several things. It is a logical framework where multiple logics can be defined and related. It is also a system implementation with support for interactive proof and automated reasoning. Additionally, it is a logical toolkit that can be used to develop new formal applications. Finally, MetaPRL has a semantic connection to programming languages, that allows the system to be used as a logical programming environment, where programs are constructed as a mixture of specifications, implementations, and verifications.
The logical theories developed in the MetaPRL system include several variations of the NuPRL type theory, a constructive ZF set theory, including an embedding of such set theory into the type theory, and others. MetaPRL automation procedures include a first order prover for both intuitionistic and classical logics.
We are planning to give a two-part tutorial. In the first part we plan to to give a high-level overview of the system and its features.
In the second part of the tutorial we want to show how one installs and starts using the system. We plan to demonstrate adding a new theory to the system and proving a few simple theorems.
We believe that this tutorial will be sufficient to get attendees ready to start using the system on their own.
| 9:00-10:30 | Overview of the MetaPRL system and its features. |
| 10:30-11:00 | Coffy break |
| 10:30-11:30 | Installing and compiling MetaPRL. |
| 11:30-12:30 | Example: Implementing first-order logic in MetaPRL. |
| 12:30-2:00 | Lunch |
| 2:00-3:30 | Example: Implementing first-order logic in MetaPRL (continued), embedding it into type theory and adding proof automation to it. |
| 3:30-4:00 | Coffy break |
| 4:00-6:00 | Example: Implementing first-order logic in MetaPRL, embedding it into type theory and adding proof automation to it (continued). |