[FOM] Logiweb

[Klaus Ebbe Grue]

I am happy to announce the release of the "Logiweb" system.

Logiweb is a system for creating a world wide web of theorems and proofs.

At present, the system is installed at
* http://logiweb.eu/
* http://logiweb.imm.dtu.dk/
   http://www.topps.diku.dk/logiweb/

To try Logiweb without installing any software, go to one of the urls 
marked with an asterisk and run the tutorial.

Logiweb is available under the GNU public license and can be downloaded 
from any of the sites listed above.



Features

User defined grammar. You may decide e.g. to write 'all X : Y' to get a 
universal quantifier.

User defined rendering. You may decide e.g. to render 'all X : Y' as
'\forall X \colon Y'.

User defined proof checker. You may define your own proof checker and 
publish it on Logiweb. Or you may decide to use a proof checker published 
on Logiweb by somebody else. For a sample proof checker and some sample 
proofs go to http://logiweb.eu/logiweb/page/check/fixed/body/index.html 
and click 'PDF'.

User defined logic. You may define your own axiomatic system. Or you may 
decide to use an axiomatic system published on Logiweb by somebody else.

Turing complete macro expansion. You may define e.g. that < 1 , 2 , 3 > 
macro expands to 1 :: 2 :: 3 :: <>. Or you may define e.g. that x , y > 5 
macro expands to x > 5 & y > 5. Or you may define e.g. that x , y in Odd , 
Prime macro expands to x in Odd & x in Prime & y in Odd & y in Prime.

Journal quality pages. In analogy to 'web pages', anything published on 
Logiweb is a 'Logiweb page'. Logiweb pages may contain a mixture of 
arbitrary LaTeX and formal, machine verified mathematics. Users may 
utilize this to produce journal quality pages.

Standing on the shoulders of others. Logiweb pages may reference 
previously published Logiweb pages. Definitions, lemmas, proofs, axiomatic 
systems, proof checkers, macros, etc. on referenced pages can be used on 
referencing pages.

Secure publication. Once published Logiweb pages get a unique identifier 
by the system (base on a RIPEMD-160 global hash key). After publication, 
pages may be mirrored, and pages continue to exist as long as just one 
copy remains on Logiweb. Pages cannot change once published making it 
secure to reference pages published by somebody else.

Automatic loading. When a Logiweb page is machine verified, all 
transitively referenced pages are located, fetched, and verified as well. 
Once verified pages are cached.

Reader friendly. While authors of Logiweb pages must either use a Logiwiki 
or install Logiweb locally, readers can view Logiweb pages using an 
ordinary web browser.

Axiomatic mixture. The demo proof checker which comes with Logiweb allows 
to define arbitrary axiomatic theories and to use several axiomatic 
theories on the same Logiweb page. As an example, it is possible to define 
both ZFC and NBG and to state and prove theorems in both systems on one 
Logiweb page.

Lambda calculus. The programming language of Logiweb is essentially lambda 
calculus. A few twists make the programming language efficient. Using 
lambda calculus makes it easy to formulate theorems about Logiweb 
programs.

Stand alone executables. The notion of a 'Logiweb machine' allows to 
express stand alone executables. A Logiweb machine extends lambda calculus 
with facilities for IO and interrupt processing. Each Logiweb page can 
define an arbitrary number of Logiweb machines which can be translated to 
stand alone executables when rendering the page.



Resources

To get notification about new versions of Logiweb join 
logiweb-announce at diku.dk by sending an e-mail to 
logiweb-announce-request at diku.dk with subject 'subscribe'.

To get notification about new Logiweb pages join logiweb-notices at diku.dk 
by sending an e-mail to logiweb-notices-request at diku.dk with subject 
'subscribe'.

To get help with Logiweb join logiweb at diku.dk by sending an e-mail to 
logiweb-request at diku.dk with subject 'subscribe'.

All three mailing lists are moderated.



Sincerely yours
Klaus Grue