Extension:JHilbert

From MediaWiki.org
Jump to: navigation, search
MediaWiki extensions manualManual:Extensions
Crystal Clear action run.png
JHilbert

Release status:Extension status experimental

ImplementationTemplate:Extension#type Tag
DescriptionTemplate:Extension#description Wiki inline proof verifier
Author(s)Template:Extension#username Alexander Klauer (GrafZahltalk)
Latest versionTemplate:Extension#version 9 (2012-01-05)
MediaWikiTemplate:Extension#mediawiki 1.18.0+
LicenseTemplate:Extension#license GNU General Public License 3.0 or later
Download
Installation instructions
Changelog
ExampleTemplate:Extension#example Tutorial
TagsTemplate:Extension#tags
<jh>
Hooks usedTemplate:Extension#hook
ParserFirstCallInitManual:Hooks/ParserFirstCallInit
ArticleDeleteCompleteManual:Hooks/ArticleDeleteComplete
ArticleMergeCompleteManual:Hooks/ArticleMergeComplete
ParserBeforeTidyManual:Hooks/ParserBeforeTidy
TitleMoveCompleteManual:Hooks/TitleMoveComplete

Translate the JHilbert extension if it is available at translatewiki.net

Check usage and version matrix.

Introduction[edit]

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[edit]

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[edit]

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[edit]

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[edit]

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.