Klaus Ebbe Grue
grue at diku.dk
Thu Feb 8 05:52:04 EST 2007
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
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.
User defined grammar. You may decide e.g. to write 'all X : Y' to get a
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
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
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
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.
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
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.
More information about the FOM