Compiler Tools

As part of grant FDCRGP 021220FD1651, I am developing tools that are useful for compiler construction. They are on a separate page. At this moment, the site contains a parser generator and a tokenizer generator. Some C++ libraries will follow when they seem mature.


Geo is a theorem prover, based on geometric resolution. The calculus is described in a joint IJCAR 2006 paper with Jia Meng, which can be downloaded from here


Geo III is new version of Geo, which aims to implement 3-valued logic. See here.

Simple Proof Checker

The proof checker is able to check natural deduction proofs using an arbitrary first-order theorem prover. The theorem prover can be selected through the first parameter. The proof to be checked is given in the second parameter. For each step in the proof, the proof checker creates an input file (in TPTP), and sends it to the theorem prover. The tool supports a weak form of higher-order logic. The program can be downloaded from Piotr Witkowski's homepage .

Constraint Solving

The most critical part of Geo III is a constraint solver which is used for checking if a rule is applicable to a partial model. Since I believe that the implementation is efficient enough to be used stand-alone, it has a page of its own.

Encryption with Rijndael

An implementation of the Rijndael-encryption scheme in C++. The user interface is primitive. The program asks whether you want to decrypt or encrypt, after that it asks for a key. If you want to encrypt it reasks for the key. Finally, it asks for an inputfile and an outputfile. It encrypts about 1Mbyte/second on an 800Mhz Pentium.

Note that Rijndael is a block cypher. As a consequence, repetitions in the input, may cause repetitions in the output. If you don't want that, you could compress the input before encrypting.

WARNING! If you encrypt a file and forget the key, then the file is gone.

The algorithm is based on the description of Rijndael in Joan Daemen, Vincent Rijmen, The Design of Rijndael, Springer Verlag, 2002.