[mizar] Mechanized Mathematics and Its Applications 2002, Vol. 2 Online

["Pauline N. Kawamoto" <pauline@cs.shinshu-u.ac.jp>]

Announcing the electronic version of "Mechanized Mathematics
and Its Applications", Vol. 2 at:

  
http://markun.cs.shinshu-u.ac.jp/mizar/mma.dir/2002/v2_toc.html

Contents
--------

  1.  "Algebraic Requirements for the Construction of
Polynomial Rings",
       Robert Milewski and Christoph
Schwarzweller

       Abstract - The Mizar construction of
polynomials with an arbitrary 
       number of variables has been
described in [8].  In this paper, we present 
       an alternative approach for
formalizing polynomials with one variable.  
       This approach has the advantage that
quite a number of theorems 
       can be proven with fewer
requirements on the underlying coefficient 
       ring.  In addition, because
polynomials with only one variable can be 
       represented more easily, the
construction allows for more 
       straightforward proofs.

  2.  "Basic Elements of Computer Algebra in MIZAR",
Adam Naumowicz 
      and Czeslaw
Bylinski

      

        

      Abstract - In this paper we describe
special features of the 
      Mizar system which provide some elements
of computer algebra 
      and present how they strengthen the
capabilities of the Mizar
checker.

    

        

  3.  "Development of LSI Circuit for RSA
Cryptogram", Yoshinori Fujisawa 
       and Yasushi Fuwa

       Abstract - In this work, we
developed a high speed circuit for encoding 
       and decoding the RSA cryptogram and
describe the processing method 
       in this paper.  This cryptogram
is used not only for encrypting data, but 
       also for such purposes as
authentication.  However, the RSA encoding 
       and decoding processes take a long
time because they require a great 
       deal of calculations.  As a
result, this cryptogram is not suited for practical 
       use.  In order to make a
high-speed processing method, we introduce the 
       following ideas:  1. To reduce
the number of summation operations, we 
       increase the number of coding bits
used to represent a digit.  2. We propose 
       a high-speed addition operation for
handling the case in which each digit has 
       a large number of bits. 
3.  We guarantee the value of modulo operations by 
       determining the possible range and
create the corresponding parallel subtraction 
       circuits beforehand to handle these
operations.  By applying these concepts, we 
       are able to reduce processing times
compared to the previous methods.  We also 
       proved the correctness of our
proposed algorithms using the Mizar system and 
       then we developed the LSI to realize
them.

  4.  "Lim-inf Convergence and its Compactness",
Grzegorz Bancerek, Noboru Endou, 
       and Yasunari
Shidama

     

        

       Abstract - We describe the Mizar
formalization of the proof of compactness of 
       lim-inf convergence given in [W33]
according to [CCL].  Lim-inf convergence 
       formalized in [W28] is a Moore-Smith
convergence investigated in [Y6] and 
       involves the concept of nets. 
The proof is based on the equivalence of two 
       approaches to convergence in
topological spaces: filter convergence and 
       Moore-Smith (net) convergence. 
The equivalence is worked out in [Y19] and 
       different characterizations of
compactness are also given there.
         These efforts are a
continuation of the international project of formalizing the 
       theory of continuous lattices headed
by the first author.

  5.  "State Machines of Calculating Type and Their
Correctness", Hisayoshi Kunimune 
       and Yasushi
Fuwa

 

        

       Abstract - In this paper, we define
the "correctness" of a state machine based 
       on a discussion of the
"result" yielding from its final states.  For simplicity,
we 
       define a state machine called a
"calculating type state machine" that can calculate 
       a simple issue and show some
examples of correct calculating type state machines.

                                 
Pauline N. Kawamoto (Aiura)
                                 
AMU - Nagano Circle and Mizar Japan