Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant

Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, and Aleksey Nogin.
Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant.
In David Basin and Burkhart Wolff, editors, 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003). Emerging Trends Proceedings, pages 29–39. Universität Freiburg, 2003.
PDF (208 KB), PostScript (172 KB).

Abstract

No proof assistant can be considered complete unless it provides facilities for basic arithmetical reasoning. Indeed, integer theory is a part of the necessary foundation for most of mathematics, logic and computer science. In this paper we present our approach to implementing arithmetic in the intuitionistic type theory of the MetaPRL proof assistant. We focus on creating an axiomatization that would take advantage of the computational features of MetaPRL type theory. Also, we implement the Arith decision procedure as a tactic that constructs proofs based on existing axiomatization, instead of being a part of the ``trusted'' code base.

Back to my publications

Last update: Friday, December 05, 2003 by Aleksey Nogin (e-mail: nogin+web@cs.caltech.edu)