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
(I am working on a new version,
that uses 3-valued logic.
Checker for Partical Classical Logic
which checks reasoning rules and equivalences for the two sequent
calculi for PCL. It works by exhaustively enumerating all possible
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
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:
The package contains C++ sources, a few examples, and a .pdf manual.
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
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.
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.
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.
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
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.