Fresh from the Labs

John Knight

Issue #172, August 2008

Hilbert II (www.qedeq.org)

Here's one for the mind-bending category. In this age of shared information and decentralization comes another cool addition to the realm of shared consciousness. Hilbert II attempts to resurrect and build on the ideals of a near dead project, QED (check the link at the end for a copy of QED's manifesto). Hilbert II's goals are:

...decentralised access to verified and readable mathematical knowledge. As its name already suggests, this project is in the tradition of Hilbert's program....Hilbert II wants to become a free, world-wide mathematical knowledge base that contains mathematical theorems and proofs in a formal correct form. All belonging documents are published under the GNU Free Documentation License. We aim to adapt the common mathematical argumentation to a formal syntax. That means, whenever in mathematics a certain kind of argumentation is often used, we will look forward to integrate it into the formal language of Hilbert II. This formal language is called the QEDEQ format.

Hilbert II provides a program suite that enables a mathematician to put theorems and proofs into that knowledge base. These proofs are automatically verified by a proof-checker. Also, texts in “common mathematical language” can be integrated. The mathematical axioms, definitions and propositions are combined to so-called QEDEQ modules. Such a module could be seen as a mathematical textbook that includes formal correct proofs. Because this system is not centrally administrated and references to any location in the Internet are possible, a world-wide mathematical knowledge base could be built. Any proof of a theorem in this “mathematical web” could be drilled down to the very elementary rules and axioms. Think of an incredible number of mathematical textbooks with hyperlinks, and each of its proofs could be verified by Hilbert II. For each theorem, the dependency of other theorems, definitions and axioms could be easily derived.

The Complex World of Mathematical Collaboration through Hilbert II

Installation

First things first, Hilbert II is a Java-based program. We generally try to avoid Java-based projects because this is Linux Journal, not “Platform-Neutral Java Webstart Journal”, but the cooler projects are definitely worth examining, and besides, it does have a Linux-specific version. For the lazy, there is a webstart version that can be launched from your browser (see the link at the end of this section), which requires you to have the Java browser plugins installed. For the Linux version, the precondition for a working prototype is a Java Runtime Environment, at least version 1.4. Hilbert II uses LaTeX for a lot of its functions, and there are some potential bugs that frequent users may run into, so check the Web site for further information on possible LaTeX requirements.

Head to the Download section of the Web site and download the Linux tarball. Extract it to your directory of choice, and open a terminal in the new qedeq directory.

At the console, enter:

$ ./qedeq_se.sh  

Or, if that doesn't work, enter:

$ sh qedeq_se.sh

Usage

Hilbert II works around XML files, and you'll need some of these XML files to get started. If you choose File→Load from web, a default file is provided from which you can begin to experiment. If you look in the main window, there's a tab called QEDEQ. Clicking on any entry on the left displays its nuts and bolts in this tab. Under Tools→LaTeX to QEDEQ, you can start playing around with your own formulae, and under Check→Check Mathematical Logic, you can make sure that your syntax and so on check out. To export your work for the world to see, going to Transform→Create LaTeX output creates a new LaTeX .tex file in the generated folder under qedeq.

But from here, you're on your own, because I haven't got a clue what I'm talking about in this world of advanced mathematics and formulae (and I've probably said something wildly inaccurate in the process of writing this section). However, I'm keen to see the results of this academic collaboration, where ideally knowledge should keep advancing and continue to be built upon, and I hope to see more of these mind-bending shared-consciousness projects.

Ever been stuck working on a text-only mailing server and wished you had some sort of decent gaming distraction? Well, you have a lot of options, such as adventure text games and moon-buggy, but my favorite discovery is vitetris, a Tetris clone with full color and many options. According to the vitetris Web site:

vitetris is a terminal-based Tetris clone by Victor Nilsson. Gameplay is much like the early Tetris games by Nintendo. Features include:

  • Configurable keys

  • Highscore table

  • Two-player mode with garbage

  • Network play

  • Joystick (gamepad) support on Linux

It has been tested on Linux, Cygwin, NetBSD and a few other UNIX-like systems. Library dependencies are minimal (only libc is required), and many features can be disabled at compile time.

vitetris provides two-player Tetris fun without graphics.

Installation

For those who prefer binaries, included at the Web site are links to RPM packages and some tarballs built with gcc 3.4.6 for i486 Linux on Slackware 11.0. However, vitetris has very few dependencies, and 99% of you should be able to compile it from the source tarball (saving you from some of the inevitable binary incompatibility). Indeed, this is the easiest and most trouble-free compilation I've encountered in a long time, so I recommend compiling it.

Grab the latest tarball from the project's Web site, extract the contents, and open a terminal in the new folder. Once inside the vitetris directory, enter the commands:

$ configure
$ make

and, as root or sudo:

# make install

Once compiled, typing tetris at the command line loads the game.

Usage

Once inside the game, you'll see a heap of cool options. For instance, you can change the height of the level you're in, enable rotation in both clockwise and counter-clockwise directions, and switch between game modes. These two game modes enable or disable attacking the other player with completed lines and adding them to the bottom of their stack (game mode A is for attacking enabled, and B is for disabled). To start a game by yourself, choose 1 Player Game, and choose your difficulty level and game height to begin. On your keyboard, the left and right arrows move each piece left and right; the up arrow rotates the piece on screen; the down arrow makes a “soft drop”; and the spacebar makes a “hard drop”, straight to the bottom of the screen.

If you want to change the keys or switch between rotation methods and so on, you can to that from the Options menu. If you want to play a two-player game, you also have to define Player 2's keys here. If you're having any problems displaying vitetris in your console and want to change the game's colors, or even switch to a monochrome mode, those options are available in the Options menu as well.

Ultimately, vitetris is a great Tetris clone by itself, but coupled with the fact that it runs on the command line without graphics, vitetris is a great addition to any system and will be a nice distraction the next time the X Window System won't start!

This was the craziest project I came across this month! Tetuhi is basically a program that takes an image and generates a game around it, but its appeal doesn't end there. Aside from making landscapes from parts of the image, Tetuhi also creates characters from other parts of the image, as well as other objects, such as food, ammo, friends and enemies, which all wriggle and move about as the engine morphs sections of the original image. On top of all that, it also has a dynamic and adaptive rule set with changing game modes—meaning each game and image may be truly random and different from the last.

I realise this crayon drawing itself doesn't show off Tetuhi's capabilities, but imagine that the hills and trees are pulsating in front of you and you are driving the sun....No, I'm not on mushrooms!

Installation

Tetuhi is definitely something that is still in development, so the usual configure && make && make install won't do you much good here. In terms of requirements, you need up-to-date versions of Python, GCC, Pygame, the Python Imaging Library, PyYAML and the Gnu Scientific Library. Once you've got those installed, head to the Tetuhi Web site and grab either the latest tarball or the latest code from the GIT repository.

Once you have either of those, extract it (if you have the tarball), and look at the directories c, img-c and perceptron. Open a terminal, and enter each one of these directories and run the commands:

$ make

and, as root or sudo:

# make python-install

This should work in all three directories without errors. If not, make sure you have all of the previously mentioned libraries installed and up to date.

Usage

Now that the compiling is out of the way, head back to the main tetuhi directory, and enter the command:

$ ./tetuhi nameofimagehere.jpg

If everything has compiled properly, an image with some crazy instructions should appear on screen, walking you through the first steps of the game. The best types of images to use are those with simplicity, such as stark backgrounds with bold elements at the forefront. Included on the Tetuhi Web page is a link to a tarball containing sample images for testing. My favorite is “hills-cars.jpg”, whose line of land, trees and a car pulses and gyrates, while you control a wiggling sun—making for the trippiest game experience I've had in some time. Once you've enjoyed the first few plays, you may want to make a symlink to a pathed directory so that you don't have to keep entering Tetuhi's source directory.

Although the games themselves are rather simplistic (and lame in most cases), it's the implications of the image manipulation that are of real interest here. I can see parts of the code foundation making it into much larger-scale projects in the gaming and multimedia area in the future. Tetuhi's creator, Douglas Bagnall, is making particular efforts so that Tetuhi can be included on the One Laptop Per Child XO laptop, so it'll be interesting to see what kind of games and drawings children around the world will come up with to play in connection with Tetuhi's game rules.

Check out some of Douglas' other crazy projects at halo.gen.nz.

John Knight is a 23-year-old, drumming- and climbing-obsessed maniac from the world's most isolated city—Perth, Western Australia. He can usually be found either buried in an Audacity screen or thrashing a kick-drum beyond recognition.