Hands-on course "Introduction into formal computer-aided reasoning and 
the MetaPRL theorem prover"

Jason Hickey and Aleksey Nogin, California Institute of Technology

Summary.

This course will teach the basics of a formal proofs and demonstrate how 
the formal proof process can be implemented in a computer proof 
assistant, MetaPRL. We will show how to define a logic as a system of 
axioms, and then use the logic to perform proofs both interactively and 
automatically. The course will include examples from first-order logic 
and type theory, and will include defining these logics as well as 
defining proof search procedures using tactics.  The course will also 
show how different logics and logical theories can be related; the 
Curry-Howard isomorphism will be used as an example.

We expect that after taking our course students will be able to install 
and use the MetaPRL system on their own. This course is going to be 
somewhat similar to the "Type Theory and Formal Methods" course taught 
by Aleksey Nogin at Caltech (see 
http://mojave.cs.caltech.edu/nogin/cs101c-03/).

Relevance to NASSLI Areas.

This course should be useful to students interested in logic, as it will 
show how different logical theories could be applied to and automated in 
a modern theorem proving system. The students will learn how to use the 
MetaPRL system to help write formal proofs in arbitrary logical 
theories, which could be useful in students' future research.

The ability to define a new system of axioms and inference rules, and 
have a computing system help with developing formal proofs (both in 
automated and user-driven interactive modes) can also be helpful to 
students interested in applying logical methods to linguistics.

Finally, computer science students will have a chance to learn about 
formal methods and how logical methods can be used in computer science.

Background Information.

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.