X.: MetaPRL — A modular logical environment (2009)
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
Abstract. MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project...
Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant ⋆ (2008)
Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, Aleksey Nogin
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...
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
, Christoph Kreitz 2, Vladimir N. Krupski 4, Lori Lorigo 2, Stephan Schmitt 5, Carl Witty
A Listing of MetaPRL Theories 1 (2007)
Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, Xin Yu
This document contains a listing of most of the MetaPRL logical theories. It is generated automatically on a daily basis. To get the latest version, go to
Integration of decision procedures into high-order interactive provers / (2006)
"A dissertation submitted to the Graduate Faculty in Computer Science ..."
A Listing of MetaPRL Theories 1 (2006)
Jason Hickey, Brian Aydemir, Yegor Bryukhov, Alexei Kopylov, Aleksey Nogin, Xin Yu
This document contains a listing of most of the MetaPRL logical theories. It is generated automatically on a daily basis. To get the latest version, go to
Implementing and Automating Basic Number Theory In MetaPRL Proof Assistant (2003)
Yegor Bryukhov, Alexei Kopylov, Vladimir Krupski, Aleksey Nogin
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,...
MetaPRL — A Modular Logical Environment (2003)
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
Abstract. MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project...
MetaPRL — A Modular Logical Environment (2003)
Jason Hickey, Aleksey Nogin, Robert L. Constable, Brian E. Aydemir, Yegor Bryukhov, Richard Eaton, ...
Abstract. MetaPRL is the latest system to come out of over twenty five years of research by the Cornell PRL group. While initially created at Cornell, MetaPRL is currently a collaborative project...