[Prev][Next][Index][Thread]
Special issue on Mechanising and Automating Mathematics
Call for Papers
JOURNAL OF AUTOMATED REASONING
Special issue on Mechanising and Automating Mathematics
>From its begin, to its end, the 20th century provided fascinating
questions and important results in the foundations and automation of
mathematics. The first half of the 20th century saw the birth of
Hilbert's dream concerning the derivation of true formulae, Goedel's
incompleteness result which shattered Hilbert's dream, lambda
calculus, type theory, logical and set theoretical paradigms whose aim
was to give a solid and expressive foundation of mathematics without
suffering from the paradoxes. In the second half of the 20th century,
computers found a powerful role in the logical foundations of
mathematics, and provided complementary and indispensible tools for
reasoning about and representing mathematics. When in 1967, N.G. de
Bruijn started his programme of Automating Mathematics (Automath), he
was told his project will fail by Goedel's result. It seemed then,
that all the confusion that reigned at the begin of the 20th century
in the logical foundations of mathematics, had surfaced again in the
automation of mathematics. But since, the area of automating and
mechanising mathematics, has been fascinating and has given birth to
many useful tools, techniques, and systems.
This special issue will be devoted to the different approaches in
mechanising and automating mathematics. In particular, we are
interested in the following:
+ The (semi-) automation of mathematics using any of the
well-established theorem provers and automated reasoning systems
(e.g., HOL, Coq, Automath, Isabelle, ALF, ELF, PVS, Nqthm, Theorema,
VSE, Omega, etc.).
+ Computerized repositories for the representation of mathematics
using any of the mathematical representation methods, languages and
tools (e.g., QED, Mizar, OMDoc, MathML, mathematical vernaculars,
etc.).
+ Formal languages and techniques (from e.g., type theorym term
rewriting, logic, and category theory, etc.) used for the
mechanisation, automation and computerisation of mathematics.
Manuscripts emphasizing original results, key open issues, progress
made and current challenges in the mechanisation, automation and
computerisation of mathematics are of particular interest.
Manuscripts should be unpublished works and not submitted elsewhere.
Revised and enhanced versions of papers published in conference
proceedings that have not appeared in archival journals are eligible
for submission. All submissions will be reviewed according to the
usual standards of scholarship and originality. Information on JAR
submissions can be found at URL http://www-unix.mcs.anl.gov/JAR/.
Please format your submissions using JAR macros (available at
http://www.wkap.nl/kaphtml.htm/STYLEFILES).
Submissions should be sent to the guest editor in postscript format,
preferably gzipped and uuencoded. In addition, please send as plain
text, the title, authors, abstract, and contact information for the
paper. The submission deadline is 10 May 2002.
Guest Editor:
Fairouz Kamareddine, Heriot-Watt University, Edinburgh, Scotland,
email fairouz@cee.hw.ac.uk
This information is available on the web at:
http://www.cee.hw.ac.uk/~fairouz/automath2002/AR.html