Bliksem

Bliksem is a resolution-based theorem prover, written in C. It was mostly written in 1998-1999. By now it has become pretty outdated, but it seems that people are still using it, so it stays on the web.

Geo

Geo is a theorem prover, based on geometric resolution. The calculus is described in a joint IJCAR 2006 paper with Jia Meng. You can also download it here here under 2006.

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 .

Parser Generation

Maphoon is an LALR-parser generator that I wrote in 1989 when I was a student. The parser of Bliksem is generated by Maphoon. (But Bliksem can also be compiled without it.) This version of Maphoon obsolete and there is no reason to download it, unless you still use Bliksem.

This is maphoon2008b. It is a parser generator written in C++. It generates a bottom up (LALR) parser in C++. It features are:

  1. True support of C++ and object-oriented programming style. Since nearly every C program is also a C++ program, every parser generator that can generate C programs, can also generate C++ programs. But in this way, the advantages of C++ cannot be used in the parser. Maphoon treats tokens as true C++-objects. The user does not have to worry about allocation and deallocation of objects, and there is no need to deal with polymorphism through pointer casts. The parser is generated in a namespace that the user can specify. This may be useful in big projects that need several parsers.
  2. Run time definition of operators. If one wants to be able to define infix/postfix/binary operators at run time, one needs a mechanism for deciding shift/reduce conflicts at run time. In maphoon, this mechanism is provided by allowing reductions to refuse. If there is a shift/reduce conflict, the parser will first try to reduce. If the reduction refuses, the parser will shift. The reduction can look at the table of defined operators and their priorities, when making its decision. In this way, operators can be defined at run time.
The package contains C++ sources, a few examples, and a .pdf manual. (Feb 2010)

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.

Compute Sunset-Sunrise Times

Here is a C-program that computes sunset/sunrise times. The interface is primitive, but the times are accurate up to the minute. Download.