Extension:JHilbert

MediaWiki extensions manual - list

JHilbert Release status: experimental
Implementation	Tag
Description	Wiki inline proof verifier
Author(s)	Alexander Klauer (GrafZahlTalk)
Last version	9 (2012-01-05)
MediaWiki	1.18.0+
License	GPL3+
Download	Project page Download master snapshot Git [Help] Commit history Installation instructions Changelog
Example	Tutorial
Tags <jh>
Hooks used ParserFirstCallInit ArticleDeleteComplete ArticleMergeComplete ParserBeforeTidy TitleMoveComplete
Check usage (experimental)

Introduction

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).

Credits

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.

Usage

A tutorial for newcomers is available! (same tutorial on Wikiproofs.)

You can add JHilbert code between JHilbert tags <jh>…</jh>. See the documentation for the syntax.

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 Interface and User interface namespaces are interpreted as interface modules.

Download instructions

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.

Installation

• Unpack the source archive.
• If you don't want to use the pre-compiled JAR archive, build the JAR with

mvn package

in the directory with the pom.xml file. 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/JHilbert subdirectory of the archive to your MediaWiki extensions directory. There should be three PHP files in the jh directory, JHilbert.php, JHilbert.body.php, and JHilbert.i18n.php.
• 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.
• Enjoy.