Back to my publicationsAleksey Nogin
Theory and Implementation of an Efficient Tactic-Based Logical
Framework.
Ph.D. Thesis, Cornell University. August 2002.
PDF
(762KB), PostScript (1003KB).
Formal methods are successfully used in a wide range of applications — from hardware and software verification to formalizing mathematics and education. However their impact is limited and is very far from realizing the full potential of formal methods. Our investigation of these limitations shows that they can not be avoided by simply fine-tuning existing tools and methods. We demonstrate the need to concentrate on improving and extending the underlying theory and methodology of computer-aided formal reasoning.
This thesis explores both practical and theoretical aspects of achieving these improvements; we present solutions for some of the outstanding problems and substantial improvements for others. In particular, we improve axiomatizations of the extant logics to make them more accessible to both users of the system and proof automating procedures. We also present methods for very significant speedup of the proof search process. Such additional speed means not only that the theorem prover will work faster, but also users can now take advantage of more advanced proof automation procedures that would have been prohibitively slow otherwise.
This thesis also demonstrates how these wide ranging practical and theoretical results can be brought together in a more efficient and more generic tactic-based formal system. In particular, we present a generic derived rules mechanism and explain how such a mechanism can facilitate practical modularization of a formal system. We also present several approaches to establishing a generic layer of proof automation procedures (tactics) that apply to a wide variety of logical theories. Most of the ideas presented in this thesis were implemented in the MetaPRL logical framework taking advantage of an existing modular flexible design and making it even more modular and more flexible.
After implementing these ideas in the MetaPRL logical framework, we use that system to improve a formalization of NuPRL intuitionistic type theory. In particular, we show how to modularize an axiomatization of a quotient type thus creating a formalization capable of expressing important concepts that were impossible to express in the original monolithic axiomatization. We also show how to add a limited form of classical reasoning to an intuitionistic type theory in a way that preserves many constructive aspects of the theory. Several theorems in this thesis were formally proven in the MetaPRL system.
Last update: Wednesday, January 07, 2004 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)