Re: New Mizar articles

Dear All,

the Mizar remote verification/solving/presentation services at
http://mws.cs.ru.nl/~mptp/MizAR.html and
http://mizar.cs.ualberta.ca/~mptp/MizAR.html have now been updated to
include the latest MML version 4.181.1147. I also added to Emacs a
function (mizar-atp-review-proofs) for ATP-based article reviewing
that calls ATPs to justify all toplevel @proofs independently (with
the whole MML). Sometimes such proofs are simpler.

Best,
Josef Urban

On Wed, Feb 22, 2012 at 9:13 AM, Adam Grabowski <[email protected]> wrote:
>  Dear All,
>  together with the latest official version of the Mizar system
> (7.13.01, MML version 4.181.1147) the following new Mizar articles
> are available:
>
> 1133. ZMODUL01
>     $\mathbb Z$-modules
>      by Yuichi Futa, Hiroyuki Okazaki and Yasunari Shidama
>     Received September 5, 2011
> 1134. MORPH_01
>     Morphology for Image Processing, Part {I}
>      by Hiroshi Yamazaki, Czes\l aw Byli\'nski and Katsumi Wasaki
>     Received September 21, 2011
> 1135. NDIFF_4
>     The Differentiable Functions from $\mathbbR$ into ${\mathbbR}^n$
>      by Keiko Narita, Artur Korni\l owicz and Yasunari Shidama
>     Received September 28, 2011
> 1136. MATRIX17
>     Some Basic Properties of Some Special Matrices, Part {III}
>      by Xiquan Liang and Tao Wang
>     Received October 23, 2011
> 1137. INTEGR19
>     Riemann Integral of Functions from $\mathbbbR$ into $n$-dimensional Real
>     Normed Space
>      by Keiichi Miyajima, Artur Korni{\l}owicz and Yasunari Shidama
>     Received October 27, 2011
> 1138. EC_PF_2
>     Operations of Points on Elliptic Curve in Projective Coordinates
>      by Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima and Yasunari Shidama
>     Received November 3, 2011
> 1139. TOPALG_6
>     Fundamental Group of $n$-sphere for $n \geq 2$
>      by Marco Riccardi and Artur Korni{\l}owicz
>     Received November 3, 2011
> 1140. BORSUK_7
>     The {B}orsuk-Ulam Theorem
>      by Artur Korni{\l}owicz and Marco Riccardi
>     Received November 3, 2011
> 1141. PDIFF_9
>     Higher Order Partial Differentiation
>      by Noboru Endou, Hiroyuki Okazaki and Yasunari Shidama
>     Received November 20, 2011
> 1142. DESCIP_1
>     Formalization of the Data Encryption Standard
>      by Hiroyuki Okazaki and Yasunari Shidama
>     Received November 30, 2011
> 1143. MMLQUERY
>     Semantic of MML Query
>      by Grzegorz Bancerek
>     Received December 18, 2011
> 1144. MENELAUS
>     Routh's, {M}enelaus' and Generalized {C}eva's Theorems
>      by Boris A. Shminke
>     Received January 16, 2012
> 1145. SCMYCIEL
>     Simple Graphs as Simplicial Complexes: the {M}ycielskian of a Graph
>      by Piotr Rudnicki and Lorna Stewart
>     Received February 8, 2012
> 1146. NTALGO_1
>     Extended Euclidean Algorithm and CRT Algorithm
>      by Hiroyuki Okazaki, Yosiki Aoki and Yasunari Shidama
>     Received February 8, 2012
> 1147. RATFUNC1
>     Introduction to Rational Functions
>      by Christoph Schwarzweller
>     Received February 8, 2012
>
>  Regards,
>  Adam Grabowski
>  Library Committee of the Association of Mizar Users