Skip to main content
PRL Project

Arithmetic module for MetaPRL: rules and Arith tactic

by Yegor Bryukhov

Both arithmetic tactics (Arith and SupInf) in Nuprl do not really construct proofs of arithmetic facts but just check according to particular algorithms. This approach unavoidably extend the amount of trusted code moreover it stands on mathematical facts that was not explicitly formalized in the system(theory). In MetaPRL we attempted to provide tactic that can construct formal proofs of certain arithmetic problems.

In this talk we'll briefly discuss:
* Current set of arithmetic rules for MetaPRL implementation of Nuprl Type Theory
* The main idea of Arith procedure and its limitations
* Current state of its implementation in MetaPRL
* How to extend this procedure beyond Nuprl Type Theory?
* What is the next possible step? - rational numbers and SupInf