Release status: experimental
|Description||Wiki inline proof verifier|
|Author(s)||Alexander Klauer (GrafZahltalk)|
|Latest version||9 (2012-01-05)|
|License||GNU General Public License 3.0 or later|
|Translate the JHilbert extension if it is available at translatewiki.net|
|Check usage and version matrix.|
JHilbert is a verifier for automated theorem proving. This wiki integration extension, combined with JHilbert's modular design allows the creation of a wiki with formalisable and formally verifiable content. Traditionally, such content would be mathematics. In theory, however, all kind of content amenable to formalisation should be possible.
JHilbert is currently in use on Wikiproofs (not a Wikimedia project).
The namesake of JHilbert is David Hilbert whose idea it was to formalise as much as possible of the body of extant mathematics. The highly general logic which drives JHilbert was invented by Norman Megill who maintains a large database of proofs based on his system, see metamath.org. Then Raph Levien devised a system to make Metamath suitable for collaborative use and implemented it in his Ghilbert software, written in python. JHilbert started out as a Java reimplementation of Ghilbert and has retained large parts of Ghilbert's original design.
Without these three people, JHilbert would not exist today.
The author would also like to thank Mel O'Cat for interesting discussions.
The code is evaluated for the Wiki page as a whole, so you can have as many
<jh>…</jh> tag groups as you like. For example, you can insert as much "normal" wiki text between JHilbert proof steps as you like.
Whether your JHilbert code is evaluated as proof module or interface module code depends on the current page's namespace. Pages in the main and in the
User module namespace are interpreted as proof modules, while pages in the
User interface namespaces are interpreted as interface modules.
Please download the latest JHilbert source tarball as gzipped tar file. If you have trouble unpacking the gzip file, please use the zip archive instead. Unless you want to build the JHilbert server yourself, you can also download a pre-compiled JAR archive.
- Unpack the source archive.
- If you don't want to use the pre-compiled JAR archive, build the JAR with
- in the directory with the
pom.xmlfile. You'll need a java development kit and the Apache maven project builder.
- Start a JHilbert server with
java -jar jhilbert-devel.jar -d
- If you run the jar without arguments, you'll get a list of options and switches.
- Copy the
src/main/php/mediawiki/extensions/JHilbertsubdirectory of the archive to your MediaWiki extensions directory. There should be three PHP files in the
- Add the following to LocalSettings.php:
# Extra namespaces define('NS_INTERFACE', 100); define('NS_INTERFACE_TALK', 101); define('NS_USER_MODULE', 102); define('NS_USER_MODULE_TALK', 103); define('NS_USER_INTERFACE', 104); define('NS_USER_INTERFACE_TALK', 105); $wgExtraNamespaces[NS_INTERFACE] = 'Interface'; $wgExtraNamespaces[NS_INTERFACE_TALK] = 'Interface_talk'; $wgExtraNamespaces[NS_USER_MODULE] = 'User_module'; $wgExtraNamespaces[NS_USER_MODULE_TALK] = 'User_module_talk'; $wgExtraNamespaces[NS_USER_INTERFACE] = 'User_interface'; $wgExtraNamespaces[NS_USER_INTERFACE_TALK] = 'User_interface_talk'; require_once( "$IP/extensions/JHilbert/JHilbert.php" );
- Of course, you may give the new namespaces numeric identifiers different from those used in this example.
- The JHilbert server uses the MediaWiki API to load dependencies. Please do not disable the API.