# 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.