KnowledgeBase » 
SEMINAR
» ID = 560
Arithmetic module for MetaPRL: rules and Arith tactic
by Yegor Bryukhov
2001-2002
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