[mizar] Computer Reconstruction of the Body of Mathematics

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Dear All,

I'd like to announce a call for papers for a special issue of Studies in 
Logic, Grammar and Rhetoric on Computer Reconstruction of the Body of 
Mathematics.

Best regards,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================

                             Call for Papers
     for a Special Issue of Studies in Logic, Grammar and Rhetoric
         on Computer Reconstruction of the Body of Mathematics

Special Issue Editors: Adam Grabowski and Adam Naumowicz

http://mizar.uwb.edu.pl/slgr.html

   Since the inception of first systems designed  for  developing  mathematical
proofs  in  a  computer-based  environment  the  research on automated  theorem
proving and proof  checking  has produced numerous proof-assistant tools. Their
involvement  in  large-scale  formalization  projects  revealed  that practical
formalization of whole theories, complete mathematical monographs or especially
challenging  proofs  requires  a  substantial  amount of dedicated work. It has
become  evident  that  for  this  sort  of  task  accumulating and distributing
previously formalized data is indispensable.
   In this spirit the Mizar community  initiated in 1989 a long-term project of
building  a comprehensive library of formal interrelated mathematical data, the
Mizar Mathematical Library  (MML). As  of  today, MML  contains over a thousand
articles  written  by  more  than  two  hundred  authors from 13 countries that
comprise  about  50000  theorems  from  a  vast  range of mathematical domains.
Still the library might be considered  minute when compared to the huge body of
mathematics  developed  throughout the past centuries.  Admittedly, it has been
estimated  that  building  a  formal   library  to  cover  only   undergraduate
mathematics would require about 140 man-years. Therefore it has been recognized
that  developing  a  library  to  base  further  formalizations  on  is equally
essential as improving the capabilities of proof-assistance software.
   With  this  special  issue we would like to disseminate research experiences 
with  all  proof-assistant  systems  that  collect  user  contributions  in  an 
organized  manner,   attempt  to  build  proof  libraries  and  allow  for  new 
developments  on  top  of  previously   accumulated   mathematical   knowledge. 
Expanding  such  libraries  and  at  the  same   time   making  them  coherent, 
well-organized  and  suitable  for querying is a highly non-trivial enterprise. 
Therefore  we  also  welcome  new  ideas  advancing  the  field  of formalizing 
mathematics,  with  special  focus  on  reconstructing  the  existing  body  of 
mathematics in a computer environment.
   We solicit original papers addressing the issues mentioned above.  Submitted
works will be subject to a usual journal  peer-review  process.  To  facilitate
typesetting,   the  submissions   should  be  in  PDF using  the  LNCS   format
(authors  of  accepted  papers  will be requested to provide the LaTeX source).
Submissions   and   any   inquiries   about  this   issue  should  be  sent  to
slgrsubmission@mizar.uwb.edu.pl.

Submission deadline: October 1, 2008
Notification of acceptance: November 1, 2008
Page limit (flexible): 20